Describe the Damas-Milner type inference in a way that a CS101 student can understand

Question

Hindley-Milner is a type system that is the basis of the type systems of many well known functional programming languages. Damas-Milner is an algorithm that infers (deduces?) types in a Hindley-Milner type system.

Wikipedia gives a description of the algorithm which, as far as I can tell, amounts to a single word: "unification." Is that all there is to it? If so, that means that the interesting part is the type system itself not the type inference system.

If Damas-Milner is more than unification, I would like a description of Damas-Milner that includes a simple example and, ideally, some code.

Also, this algorithm is often said to do type inference. Is it really an inference system? I thought it was only deducing the types.

Related questions:

• What is Hindley Miller?
• Type inference to unification problem

Answer 1

Damas Milner is just a structured use of unification.

When it recurses into a lambda expression it makes up a new variable name. When you, in a sub-term, find that variable used in a way that would require a given type, it records the unification of that variable and that type. If it ever tries to unify two types that don't make sense, like saying that an individual variable is both an Int and a function from a -> b, then it yells at you for doing something bad.

Also, this algorithm is often said to do type inference. Is it really an inference system? I thought it was only deducing the types.

Deducing the types is type inference. Checking to see that type annotations are valid for a given term is type checking. They are different problems.

If so, that means that the interesting part is the type system itself not the type inference system.

It is commonly said that Hindley-Milner style type systems are balanced on a cusp. If you add much more functionality it becomes impossible to infer the types. So type system extensions that you can layer on top of a Hindley-Milner style type system without destroying its inference properties are really the interesting parts of modern functional languages. In some cases, we mix type inference and type checking, for instance in Haskell a lot of modern extensions can't be inferred, but can be checked, so they require type annotations for advanced features, like polymorphic recursion.

Answer 2

Wikipedia gives a description of the algorithm which, as far as I can tell, amounts to a single word: "unification." Is that all there is to it? If so, that means that the interesting part is the type system itself not the type inference system.

IIRC, the interesting part of the Damas-Milner type inference Algorithm W is that it infers the most general types possible.