link to talk recording

[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 9e682cb54109593d774e9b8de8c187bb33b894a0..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) 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 remark in the original paper.
+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?