ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md

   1 ---
   2 title: "Exponential blowup when using unbundled typeclasses to model algebraic hierarchies"
   3 categories: research coq
   4 forum: https://coq.discourse.group/t/blog-post-exponential-blowup-when-using-unbundled-typeclasses-to-model-algebraic-hierarchies/289
   5 ---
   6
   7 When formalizing a proof in an interactive theorem prover like [Coq](https://coq.inria.fr/), one reoccurring issue is the handling of algebraic hierarchies.
   8 Such hierarchies are everywhere:  some operations are associative, while others commute; some types have an equivalence relation, while others also have a (pre-)order or maybe even a well-ordering; and so on.
   9 So the question arises:  What is the best way to actually encode these hierarchies in Coq?
  10 Coq offers two mechanisms that are suited to solve this task: typeclasses and canonical structures.
  11 Both can be instrumented in different ways to obtain a (more or less) convenient-to-use algebraic hierarchy.
  12 A common approach using typeclasses is the ["unbundled" approach by Bas Spitters and Eelis van der Weegen](http://www.eelis.net/research/math-classes/mscs.pdf).
  13 However as we learned the hard way in the Coq formalization of the [original Iris paper](https://iris-project.org/pdfs/2015-popl-iris1-final.pdf), this approach quickly leads to terms that seem to be exponential in size.
  14 In this post, I will explain the cause of this exponential blowup.
  15
  16 <!-- MORE -->
  17
  18 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.
  19 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.
  20
  21 ## Unbundled groups
  22
  23 A formalization of the algebraic hierarchy for groups using the unbundled approach could look as follows:
  24 {% highlight coq %}
  25 Require Import Lia ZArith.
  26
  27 (** The operations as typeclasses for overloading, without any axioms. *)
  28 Class Op (A: Type) := op : A -> A -> A.
  29 Infix "+" := op.
  30
  31 Class Unit (A: Type) := unit : A.
  32
  33 Class Inverse (A: Type) := inv : A -> A.
  34
  35 (** The algebraic classes adding the axioms, taking the operations as indices. *)
  36 Class Semigroup (A: Type) `{Op A} := {
  37   assoc a b c : (a + b) + c = a + (b + c);
  38 }.
  39
  40 Class Monoid (A: Type) `{Semigroup A, Unit A} := {
  41   id_r a : a + unit = a;
  42   id_l a : unit + a = a;
  43 }.
  44
  45 Class Group (A: Type) `{Monoid A, Inverse A} := {
  46   inv_r a : a + inv a = unit;
  47   inv_l a : inv a + a = unit;
  48 }.
  49 {% endhighlight %}
  50
  51 As usual for the unbundled approach, we end up with lots of tiny typeclasses.
  52 `Op`, `Unit` and `Inverse` serve as operators that can be overloaded.
  53 They each just take a type `A` as argument (we say they are *indexed* by the type: we can do typeclass search that, given the type, finds the instance).
  54 `Semigroup`, `Monoid` and `Group` supply the laws for these operators; they are indexed by the operators they involve and the typeclasses from which they "inherit".
  55 Taking the superclasses as indices instead of embedding them as fields simplifies typeclass search and is necessary to support diamonds in the hierarchy; see [the original paper](http://www.eelis.net/research/math-classes/mscs.pdf) for more details.
  56
  57 We use Coq's feature for anonymous implicit generalization: `` `{Semigroup A} `` adds not only a parameter of type `Semigroup A` that we don't have to name; furthermore all typeclass arguments of `Semigroup` (in this case, `Op A`) are also implicitly added as parameter.
  58 This avoids lots of repetition that the unbundled style would usually incur, [but the semantics of implicit generalization are quirky and poorly documented](https://coq.discourse.group/t/documentation-of-foo/129).
  59
  60 Next, we can show that the integers `Z` form a group:
  61 {% highlight coq %}
  62 Instance Z_op: Op Z := Z.add.
  63 Instance Z_unit: Unit Z := 0%Z.
  64 Instance Z_inv: Inverse Z := Z.opp.
  65
  66 Instance Z_semigroup: Semigroup Z.
  67 Proof. split. intros. unfold op, Z_op. lia. Qed.
  68 Instance Z_monoid: Monoid Z.
  69 Proof. split; intros; unfold op, Z_op, unit, Z_unit; lia. Qed.
  70 Instance Z_group: Group Z.
  71 Proof. split; intros; unfold op, Z_op, unit, Z_unit, inv, Z_inv; lia. Qed.
  72 {% endhighlight %}
  73 We let `lia` do most of the proving, but we have to unfold some definitions first.
  74
  75 We can also show that a product of two {semigroups, monoids, groups} is itself a {semigroup, monoid, group}:
  76 {% highlight coq %}
  77 Section prod.
  78   Context {A B: Type}.
  79
  80   Global Instance prod_op `{Op A, Op B}: Op (A * B) :=
  81     fun '(a1, b1) '(a2, b2) => (a1 + a2, b1 + b2).
  82   Global Instance prod_unit `{Unit A, Unit B}: Unit (A * B) :=
  83     (unit, unit).
  84   Global Instance prod_inv `{Inverse A, Inverse B}: Inverse (A * B) :=
  85     fun '(a, b) => (inv a, inv b).
  86
  87   Global Instance prod_semigroup `{Semigroup A, Semigroup B}: Semigroup (A * B).
  88   Proof.
  89     split. intros [a1 b1] [a2 b2] [a3 b3]. unfold op, prod_op.
  90     rewrite !assoc. reflexivity.
  91   Qed.
  92   Global Instance prod_monoid `{Monoid A, Monoid B}: Monoid (A * B).
  93   Proof.
  94     split; intros [a b]; unfold op, prod_op, unit, prod_unit;
  95       rewrite ?id_l, ?id_r; reflexivity.
  96   Qed.
  97   Global Instance prod_group `{Group A, Group B}: Group (A * B).
  98   Proof.
  99     split; intros [a b]; unfold op, prod_op, unit, prod_unit, inv, prod_inv;
 100       rewrite ?inv_l, ?inv_r; reflexivity.
 101   Qed.
 102 End prod.
 103 {% endhighlight %}
 104
 105 ## Unexpected complexities
 106
 107 Seems reasonable?
 108 Unfortunately, we have set ourselves up for some unexpectedly large terms:
 109 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!
 110
 111 {% highlight coq %}
 112 Definition test: Group (Z*Z*Z*Z*Z*Z) := _.
 113 Set Printing All.
 114 Print test.
 115 (* Lots of output. *)
 116 {% endhighlight %}
 117
 118 What is happening here?
 119 We can see that when we try to construct the proof terms more explicitly.
 120 We start by defining `Zn`, which is basically `Z^(n+1)`: a product of `n+1` times `Z`.
 121 {% highlight coq %}
 122 Fixpoint Zn (n: nat): Type :=
 123   match n with
 124   | O => Z
 125   | S n => @prod (Zn n) Z
 126   end.
 127 {% endhighlight %}
 128 Unsurprisingly, this term has size linear in `n`: the recursive case adds `@prod • Z` around the term produced for `n-1` (represented by the `•`).
 129 This means the term grows by a constant when `n` increases by 1, leading to linear complexity overall.
 130
 131 Next, we define `Op (Zn n)`:
 132 {% highlight coq %}
 133 Fixpoint Zn_op (n: nat): Op (Zn n) :=
 134   match n with
 135   | O => Z_op
 136   | S n => @prod_op (Zn n) Z (Zn_op n) Z_op
 137   end.
 138 {% endhighlight %}
 139 In the recursive case, we use `prod_op` as one might expect.
 140 Coq could infer all the arguments here, but let us take a closer look at what it would infer: what is the size of `Zn_op` as `n` grows?
 141 In the recursive case, we add `@prod_op (Zn n) Z • Z_op` around the term produced for `n-1`.
 142 This term includes `Zn n`, which we established is linear in size.
 143 When `n` increases by 1, the term grows by a linear amount.
 144 Thus, the overall term size is quadratic in `n`!
 145 Ouch.
 146 I don't know about you, but I found this surprising when I realized it for the first time.
 147
 148 The index basically repeats all the information that is already present in the recursive call:
 149 to extend a `Zn_op` by one more element, we have to repeat the full type for which we already constructed an `Op`.
 150
 151 But, you might say, quadratic complexity is not so bad.
 152 Computers are fast, we can handle that.
 153 Unfortunately, I got bad news: things get worse as our indices start nesting.
 154 Let us look at the instance for `Semigroup (Zn n)`:
 155 {% highlight coq %}
 156 Fixpoint Zn_semigroup (n: nat): Semigroup (Zn n) :=
 157   match n return @Semigroup (Zn n) (Zn_op n) with
 158   | O => Z_semigroup
 159   | S n => @prod_semigroup (Zn n) Z (Zn_op n) (Zn_semigroup n) Z_op Z_semigroup
 160   end.
 161 {% endhighlight %}
 162 How big is this term?
 163 Well, the term added as `n` increases by 1 is `@prod_semigroup (Zn n) Z (Zn_op n) • Z_op Z_semigroup`.
 164 This includes `Zn_op n`, which is quadratic -- so `Zn_semigroup` is cubic!
 165
 166 `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`.
 167 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.
 168
 169 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]
 170 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.
 171 That's 4 nested indices, and hence the terms have size `O(n^5)`.
 172 More generally speaking, the term size is *exponential* in the height of our hierarchy.
 173 That hurts.
 174
 175 [^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.
 176
 177 ## Conclusion
 178
 179 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.
 180 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.
 181
 182 In my view, this basically rules out the unbundled approach for any serious formalization effort.
 183 But what are the alternatives?
 184
 185 Instead of making superclasses indices, we could make them fields, as in:
 186 {% highlight coq %}
 187 Class Monoid (A: Type) `{Op A, Unit A} := {
 188   monoid_semigroup :> Semigroup A;
 189   id_r a : a + unit = a;
 190   id_l a : unit + a = a;
 191 }.
 192 {% endhighlight %}
 193
 194 This limits the "index depth" to 2, and thus limits term complexity to `O(n^3)`.
 195 Still not great, but at least it doesn't grow further as we add more subclasses.
 196 However, this scheme does not support diamonds in the hierarchy as instances will be duplicated.
 197 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`.
 198 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]
 199
 200 [^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.
 201
 202 Maybe there is a way to make the unbundled approach viable with some help from the proof assistant.
 203 Some way to eliminate indices would help (similar to primitive projections, but also covering operations such as `prod_op`).
 204 Or maybe the proof assistant could exploit the huge amounts of sharing that are present in these large terms.
 205 If all subterms are properly shared, I think the overall term size remains linear.
 206 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).
 207 Defeating the exponential complexity here would require exploiting the sharing in *every* pass over the term.
 208 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).
 209
 210 In Iris, we instead went with an adaptation of [this approach based on canonical structures](https://hal.inria.fr/hal-00816703v1/document).
 211 This fully bundled approach avoids indices entirely and thus maintains a linear term size.
 212 On the other hand, it comes with a lot of boilerplate code, and mixing canonical structures with typeclasses can be tricky to debug. (Unfortunately we cannot avoid typeclasses entirely as we need to have `Proper` instances in our algebraic classes.)
 213 When composing types, Iris users have to write things like `prodC (listC natC) (optionC fracC)` instead of `(list nat) * (option frac)`, which is an additional barrier of entry to an already complicated development.
 214 Also, I have to say I don't really have an intuitive grasp of canonical structure resolution, so when something does not work I don't even know how to start debugging.
 215 On the other hand, the correctness proof of the logic *and* the general proof mode infrastructure *and* a few examples verified in the logic take less than five minutes to compile in our latest Coq formalization.
 216 That's quite some speedup!
 217
 218 All in all, I think the question of how to best represent algebraic hierarchies in a proof assistant is still wide open.
 219 I am curious which ideas people will come up with!
 220
 221 #### Footnotes