= Robin Milner
{c}
<Robin Milner> presented a polymorphic type discipline and its inference algorithm in 1978. <Algorithm W> derives types from program structure while using <unification> to satisfy type constraints; suitable <let polymorphism>[let-bound] expressions receive reusable type schemes. This work is a foundation of <Hindley-Milner type inference>.<A Theory of Type Polymorphism in Programming by Robin Milner>[§4.1, Algorithm W; §4.2, syntactic soundness]{ref}
For example, an <identity function> has type $\alpha\to\alpha$. Generalizing a <let polymorphism>[let-bound] identity permits separate uses at <integer> and Boolean types, whereas one lambda-bound parameter has one shared type within its scope. The discipline therefore gives precise rules for reuse rather than treating every occurrence as independently polymorphic. Its type-soundness claim concerns specified <type safety>[runtime type errors], not every possible program failure.
Back to article page
