Type Systems

Robin Milner’s Creative Leaps

• The simple type system for the ?-calculus is truly onerous because polymorphic functions (those with variables in their principal types) have to be rewritten for each different typing. The original Pascal language suffers from precisely this problem.

Milner recognized that a surprisingly useful form of polymorphism could be added to the (simply) typed ?-calculus by adding a let construct to the language family. The extension adds one new form to the family syntax

M ::= … | (let (x M) M)

Given an expression of the form

(let (x M) N)

x can be used polymorphically in N without breaking the principal typing property. Type reconstruction can first infer the principal type of M and subsequently use a renamed version of this type (a fresh name for each distinct type variable) for each distinct occurrence of x in N.

Previous slide

Next slide

Back to first slide

View graphic version