mmmodularity!

» by Scott Kilpatrick

Ben Delaware is thinking about mixin modules for Coq as a means of modularly extending data types, theorems, and proofs. (This is a dramatic departure from the mixin modules of (Dreyer and Rossberg, 2008), where (inductive data) types may not be extended once defined. In MixML two type exports only link together if one is a subtype of the other, according to some notion of core subtyping.)

Here’s an example of Ben’s idea. (Please correct me if I’m wrong, Ben.) Consider a Coq module $M$ containing an $\mathtt{Inductive}$ definition of some object $T$, as well as a theorem $\phi$ about $T$ with corresponding proof term, $p : \phi : \mathrm{Prop}$. Another module ${\delta}M$ would be mixed in to $M$, providing extensions (i.e. new or modified constructors) of $T$, $\phi$, and $p$, resulting in a new module $M’$ that contains the fully extended type, theorem, and proof.

As Ben explained this to me, my mind immediately jumped to category theory, due to my recent exploration of inductive definitions. If inductive data types are least fixed points of functors, what are these extensions? Maybe natural transformations? Gil and I talked it through, and the natural transformation interpretation seemed plausible. I hope to investigate this idea more soon.

While Ben is attempting to flesh out his full-featured idea for Coq, I’m thinking about this category theory interpretation in the context of a simpler, HM-like type system. The specific case of extensible data types in FP, from a practical standpoint, has been tackled before, e.g., as polymorphic sum types and first-class cases (Blume et al., 2006). To my knowledge, however, there is no foundational story for this kind of extensibility in the language of category theory.

* * *

OOP aside: This kind of extensibility should seem familiar to OOPers since, essentially, that’s what classes and inheritance do. Extending a data type with new constructors is like adding new subclasses; extending a term with new cases is like adding new methods; and all the while the programmer only writes the new stuff in these extensions. In the code, each $\mathtt{instanceof}$ + downcast on an object of class $C_T$ in OOP corresponds to an elimination of (i.e. pattern match on) a term of $\mathtt{Inductive}$ type $T$ in FP. A key distinction is that such eliminating code presupposes an “open world” of subclasses in OOP but a “closed world” of constructors in FP. In more concrete terms, the FP pattern match would be ill-typed without explicitly handling any new, mixed-in constructors of the type, whereas the OOP downcast would still be well-typed.