Introduction to typing and Hindley-Milner type inference

[Vincent]

A very short introduction (10 to 20 minutes) to typing and Hindley-Milner type inference algorithm (aka. Algorithm W).

I have left the concept of unification intuitive (there is nothing about Robinson's algorithm; there are no substitutions) and simplified the expression of the algorithm (it is assumed that no same variable is bound twice).

The algorithm is here presented for a simply-typed lambda-calculus, extended with built-in constants and types (bool, int, etc ad lib).

My main sources were

• Damas, Luis; Milner, Robin (1982), "Principal type-schemes for functional programs", POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, pp. 207--212
• http://www.ii.uib.no/~bezem/INF121/ (type inference paper)