mmmodularity!

» by Scott Kilpatrick

In my search for Ph.D. programs I came upon (via everybody’s favorite Italian, Lorenzo Alvisi) the Type Systems and Functional Programming group at the newish Max Planck Institute for Software Systems in Saarbruecken, Germany. The web page for Derek Dreyer, the head of that group, was particularly revealing:

[ … ] I showed how to extend ML with support for overloading and ad hoc polymorphism through Haskell-style type classes. This work exposes deep connections between ML modules and Haskell type classes, resulting in a unifying account of the two features that encourages modularity and avoids redundancy of mechanism.

Hmm, what does that remind me of? Ah yes, my own research:

For my master’s thesis I am investigating the type systems common in two different worlds of programming, object-oriented and functional languages. Using metaclasses to achieve a notion of qualified types, I plan to show how this unifies the type systems of object-oriented and functional languages, and hopefully this will provide new illumination on the expression problem.

More concretely, I will extend a core version of Fortress to support a restricted form of metaclasses that will — combined with convenient syntax and extended inference techniques — provide mechanics similar to Haskell’s type classes.

Intrigued, I looked at some of his publications. Among them,

Derek Dreyer, Robert Harper, and Manuel M. T. Chakravarty. Modular Type Classes. In POPL ‘07.

which I had previously found but set aside in favor of Mark P. Jones’ dissertation since I’m rather unfamiliar with ML modules. Reinvigorated, I read the paper after skimming through Bob Harper’s ML book online. Turns out I should have done this sooner.

Modulo William’s somewhat subtle differentiation of ADTs from objects, modules conceptually resemble objects a great deal. That Dreyer has already illustrated an extension of a module system to support the mechanics of type classes is both frustrating and encouraging — primarily I feel quite validated, so that’s nice. Here are some thoughts that come to mind regarding their work:

• Type classes are represented as simple ML signature with a magic, reserved type component named `t`, the class parameter. Instances are ML structures that satisfy these signatures, either atomic (a simple struct) or compound (an awkward functor).
• Superclasses are represented as the union of two classes, rather than a containment. Strange, but I suppose this helps to reason about instances since they either are atomic themselves or contain atomic instances.
• Haskell only allows one class instance per type, so the implicit global importing of instances can clash with what a programmer really wants to do (say, define a zany ordering on ints). The authors address this issue with an explicit import mechanism for instances, specifically, the canonical instances. (This workaround resembles what Justin and I want to do with Fortress coercions.)
• Haskell’s source language takes simple constrained types that are translated to explicit dictionary application; the authors’ source language takes explicit `overload` expressions — resembling dictionary selector functions in Haskell — that are translated to explicit functor application. Haskell: `Eq a => …`; ML: `functor _ (A: EQ) …`.
• An analogue of Haskell’s associated types is supported for type classes like `Collects c e`.
• Care is taken to avoid the aforementioned problem of overlapping instances, where two different instances occur for the same class and type in any scope.
• They provide a formal semantics for translation and type inference. Inference is incomplete for the same reason as Haskell’s; e.g. `show (read “1”)`.

Some comparisons to my system:

• Hopefully mine will utilize Fortress’ complicated overloading semantics to address the instance scope issue, rather than require any explicit usage.
• That instances are entirely nominally-specified in my system seems to reduce the problem of checking overlap (i.e. does a trait implement some interface in different ways) to one of normal inheritance hierarchy checking.
• The domain of an object-oriented language with nominal subtyping is still fairly different from ML, and the incorporation of metaclasses to achieve type classes is still novel, as far as I know.

Certainly this work will heavily influence my own, as will the ML module system itself. Huzzah for Lorenzo Alvisi and Derek Dreyer.