From 1e1d042b8d70c628e1dcd7e3fefefad5c10aa1e4 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 16 May 2019 18:40:31 +0200 Subject: [PATCH] typo --- ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md b/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md index 47ce741..9e682cb 100644 --- a/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md +++ b/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md @@ -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] -- 2.30.2