2008-03-29

OCaml and typeful programming: an annotated bibliography (of sorts)

I cannot help but feel somewhat envious at the high level of expertise that the Haskell community display at effectively using the advanced type system the language provides. Many of the techniques are not applicable to OCaml, which lacks higher-ranked polymorphism. Some of these techniques, however, can be translated to OCaml, but these seem to be more folklore than codified practice, and finding material about it feels like a fishing expedition.

Aside: SML is as amenable as OCaml to these techniques, and some are more standard in the former than in the latter; in particular, MLton's Basis and additional libraries are a marvel of elegance and power, and in my opinion should guide OCaml's library long-term design. It would be a nice project, a re-implementation of ML's Basis for OCaml that replaced its standard library, if only to incorporate MLton's extended library.

So, for the record, here's a list of pointers (I dare not call this an "annotated bibliography") to some of the "tricks", for easy retrieval and study.

The Expression Problem

Jacques Garrigue's solution is canonical, and the basic use case for polmorphic variants. Dually, Didier Rémy uses objects.

Haskell vs. OCaml

It is known that Haskell type classes can be encoded as ML modules and functors (Kisyelov and Shan's Translucent Functors).

Existential types

The poor man's approach to existential types is to use polymorphic variants. However, although it might seem as hackery, objects encode the existential parameter via the type of self, as Oleg points out repeatedly:

Polymorphic recursion

Either through references or polymorphic records, Oleg is a master wizard:

Phantom types

There's much written about phantom types and their application to verify static lightweight capabilities. A collection of techniques and applications:

As you can see, Oleg (who really has a last name) seems to run Hindley-Milner as a background thought process. His page on ML writings and code is fully worth of study.

Edit: I found a couple of references more too good to let pass.

Edit 2: Oleg is a treasure trove of insight…

No comments: