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)