Damas-Hindley-Milner type inference algorithm implementation

19
votes

I'm looking for information about the well-known Damas-Hindley-Milner algorithm to do type inference for functional languages, especially information about implementation.

I already know how to do the Algorithm W, but I heard about recent new algorithms based on constraint generator/solver rather than usual unification. However, I can't manage to find any discussions about the implementation of those new algorithm.

Any idea where I could find some partial information on ML inference ?

1
algorithmtype-inferencehindley-milner
Are you sure that constraint generation/solving was not for type systems with subtyping, e.g. one of the HM(X) family (Hindley-Milner parameterized by a subtyping relation)? – Pascal Cuoq
I read it could be used for the HM(X) family with subtyping, but also for things like type classes (parametric polymorphism), so I'm a bit puzzled – Vinz
Type classes are somewhat orthogonal to parametric polymorphism. I think Pascal Cuoq might be correct. I'm not sure I've seen any serious alternatives to plain ol' constraint generation-and-unification for type reconstruction in Standard ML, for example. Alternative approaches would certainly become useful for the kinds of extensions that have been proposed though. – Gian
Not a 100% answer since you asked about ML, but I wonder if this is what you had heard about: Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism, Dr. Gerg˝o Érdi gergo.erdi.hu/projects/tandoori/… . As you might guess from the occurrence of the word "typeclass" this is about Haskell. – cardiff space man

1 Answers

18
votes

If you're comfortable with ML code, the best way to find these things is to simply look into the implementations in the wild. A good reference implementation is HaMLet, which is designed as more of a test platform rather than a production implementation.

Almost all serious recent discussion of these issues is going to be in scholarly venues. One paper that might be of interest is Generalising Hindley-Milner type inference algorithms.

Also, the implementations of various type systems (including let polymorphism) in Pierce's "Types and Programming Languages", as well as Appel's "Modern Compiler Implementation in ML" more closely match modern approaches to implementing this than the vanilla description of algorithm W.