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