From 9b43d6da3cee25e02c680b527f10b2dd66d4e6a4 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 15 May 2019 10:06:47 +0200
Subject: [PATCH] more editing and a new link
---
ralf/_drafts/typeclasses-exponential-blowup.md | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/ralf/_drafts/typeclasses-exponential-blowup.md b/ralf/_drafts/typeclasses-exponential-blowup.md
index f081e79..4c4c0a0 100644
--- a/ralf/_drafts/typeclasses-exponential-blowup.md
+++ b/ralf/_drafts/typeclasses-exponential-blowup.md
@@ -194,7 +194,7 @@ 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.
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 search times when performing backtracking typeclass search: a `Semigroup (A*A)` can be obtained either by searching for a `Monoid (A*A)` or via `prod_semigroup`, and in case of backtracking Coq will go through a combinatorial explosion when trying all possible ways to derive `Semigroup (A*A*A*...)`.[^2]
+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]: In genaral, such combinatorial blowups happen very easily with backtracking, and they are hard to detect in advance. This is one reason why I believe that backtracking-per-default is a bad choice for proof search.
@@ -204,6 +204,7 @@ Or maybe the proof assistant could exploit the huge amounts of sharing that are
If all subterms are properly shared, I think the overall term size remains linear.
Coq deduplicates term representation in memory, but (to my knowledge) does not exploit sharing when traversing the term (for unification or type-checking or any other purpose).
Defeating the exponential complexity here would require exploiting the sharing in *every* pass over the term.
+An alternative to opportunistically discovering and exploiting sharing might be to [bake it more deeply into metavariable inference](https://eutypes.cs.ru.nl/eutypes_pmwiki/uploads/Meetings/Kovacs_slides.pdf).
In Iris, we instead went with an adaptation of [this approach based on canonical structures](https://hal.inria.fr/hal-00816703v1/document).
This fully bundled approach avoids indices entirely and thus maintains a linear term size.
--
2.20.1