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.

• Garrigue, Jacques. Private rows: abstracting the unnamed (2006), online
• — Simple Type Inference for Structural Polymorphism (2002), online
• Overview at Lambda the Ultimate
• Rémy & Vuillon, On the (un)reality of virtual types (2000), online
• Rémy's code for the above

Haskell vs. OCaml

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

• Caml list
• Lambda the Ultimate
• A simpler encoding
• Oleg on the type of the Continuation Monad
• Oleg critiques monads on the OCaml list and Lambda the Ultimate

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:

• Oleg's explanation
• Another Oleg post
• Jacques' introduction
• Oleg's elimination
• A full and faithful encoding of Haskell existentials
• OCaml as Scheme
• Encoding via references

Polymorphic recursion

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

• Arrows, on the Caml List
• Existentials, on the Caml List
• Julien Signole's many forms of type-sound Ω
• Oleg's typed fixpoint combinators

Phantom types

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

• Oleg's sprintf on the Caml List
• Capabilities, and number-parameterized types
• Polymorphic variants and structural subtyping of capabilities
• Stepwise definition of records
• Yaron Minsky's overview
• Typed relational algebra

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…