From 371f14d738ae80bf57673d564b812953808a1f58 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 10 Jun 2021 10:00:29 +0200 Subject: [PATCH 1/1] fix some typos --- .../_posts/2019-05-15-typeclasses-exponential-blowup.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md b/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md index bc9a8c9..4c9f3cf 100644 --- a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md +++ b/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md @@ -16,7 +16,7 @@ In this post, I will explain the cause of this exponential blowup. 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 the two papers. +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? -- 2.30.2