link from old post to new

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

diff --git a/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md b/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md
index 2eda6134d0bb1005adb1fa7ee95175ac133e5829..9e682cb54109593d774e9b8de8c187bb33b894a0 100644 (file)
--- a/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md
+++ b/ralf/_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) 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.
 
 ## Unbundled groups
 
@@ -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]