add another link to Neven's material at the end

[web.git] / personal / _posts / 2019-05-15-typeclasses-exponential-blowup.md

diff --git a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md b/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
index 2eda6134d0bb1005adb1fa7ee95175ac133e5829..4c9f3cf20c58d2a74948560fb8a7d853fded7bca 100644 (file)
--- a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
+++ b/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
@@ -15,8 +15,8 @@ In this post, I will explain the cause of this exponential blowup.
 
 <!-- MORE -->
 
-I should note that this observation is not new, it already occurs in [François Garillot's PhD thesis](https://pastel.archives-ouvertes.fr/pastel-00649586).
-The goal of this post is to provide a more self-contained presentation, not requiring all the context set up in that thesis.
+I should note that this observation is not new, it already occurs in [François Garillot's PhD thesis](https://pastel.archives-ouvertes.fr/pastel-00649586), a [paper by the same author](https://hal.inria.fr/inria-00368403v2/document) and even the authors of the "unbundled" paper already note having performance problems when scaling up.
+The goal of this post is to provide a more self-contained presentation, not requiring all the context set up in that thesis and going into more details than the brief remarks in the two papers.
 
 ## Unbundled groups
 
@@ -172,12 +172,12 @@ That's 4 nested indices, and hence the terms have size `O(n^5)`.
 More generally speaking, the term size is *exponential* in the height of our hierarchy.
 That hurts.
 
-[^1]: Note that the *number* of indices does not matter, like the fact that `Monoid` has both an `Op` and a `Unit` index. That just affects the constant factor. It's the nesting of indices that gets us here.
+[^1]: Note that the *number* of indices does not matter, like the fact that `Monoid` has both an `Op` and a `Unit` index. That just affects the constant factor. It's the nesting of indices that gets us into trouble here.
 
 ## Conclusion
 
 We have seen that the number of nested indices of a typeclass has exponential impact on the size of proof terms that arise when deriving typeclass instances for compound types.
-This effect has grinded the original Iris coq development back in 2015 to a halt: compiling the correctness proof of the logic itself took around 3.5 hours and needed more than the 4GB of RAM than my laptop had back then.
+This effect has grinded the original Iris coq development back in 2015 to a halt: compiling the correctness proof of the logic itself took around 3.5 hours and needed more than the 4GB of RAM that my laptop had back then.
 
 In my view, this basically rules out the unbundled approach for any serious formalization effort.
 But what are the alternatives?
@@ -192,7 +192,7 @@ Class Monoid (A: Type) `{Op A, Unit A} := {
 {% endhighlight %}
 
 This limits the "index depth" to 2, and thus limits term complexity to `O(n^3)`.
-Still not great, but at least it doesn't grow further as we add more sublcasses.
+Still not great, but at least it doesn't grow further as we add more subclasses.
 However, this scheme does not support diamonds in the hierarchy as instances will be duplicated.
 Also, the instance we implicitly added by writing `:>`, namely that `Monoid A -> Semigroup A`, means we'll check all `Monoid` instances any time we just want a `Semigroup`.
 This leads to exponential complexity when performing backtracking typeclass search: a `Semigroup (A*A)` can be obtained either by searching for a `Monoid (A*A)` or via `prod_semigroup`, so in case of backtracking Coq will go through a combinatorial explosion when trying all possible ways to derive `Semigroup (A*A*A*...)`.[^2]