Seems reasonable?
Unfortunately, we have set ourselves up for some unexpectedly large terms:
-the instance of something like `Group (Z*Z*Z*Z*Z*Z)` grows with the fifth power as the number of `Z` increase!
+the size of an instance of something like `Group (Z*Z*Z*Z*Z*Z)` grows with the fifth power as the number of `Z` increase!
{% highlight coq %}
Definition test: Group (Z*Z*Z*Z*Z*Z) := _.
`Zn_semigroup` has an `Op (Zn n)` as index, and again the full nested term describing the operator of both semigroups that we take the product of is getting repeated each time we add just one more `Z`.
So, while `Op (Zn n)` has an index that makes it grow quadratically, `Semigroup (Zn n)` *has an index that has an index*, and grows cubically.
-To compute the complexity of our terms, we have to figure out *how nested* our indices are: with no indices (such as `Zn n` itself), the term is linear; for each extra nested index the power increases by 1.[^1]
+
+In general, to compute the complexity of our terms, we have to figure out *how nested* our indices are: with no indices (such as `Zn n` itself), the term is linear; for each extra nested index the power increases by 1.[^1]
If we look at `Group`, we see that it has a `Monoid` index which has a `Semigroup` index which has an `Op` index which has a `Type` index.
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.
}.
{% endhighlight %}
-This limits the "index depth" to 1, and thus limits term complexity to `O(n^2)`.
+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.
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.
projects / web.git / blobdiff