Type Systems
Robin Milner’s Creative Leaps continued
Explanation: in essence, the definition of x is treated like a macro (abbreviation) that is replicated for each occurrence of x in N. Of course, a language implementation only needs one copy of the code for M provided that all the different instantiations of the principal type use the same data layout.
In our simple ? language: (let (i (?x x)) (((i +) (i 2)) 2))
In a richer language of the family:
(let (append (? x,y (if (empty? x) y (cons (first x) (append (rest x) y))))
(append (cons (append (cons 1 empty) (cons 2 empty)) empty) empty))
Note: empty and cons are polymorphic constants; let is recursive.
Milner also realized he could rigorously prove a that typable programs cannot generate certain errors. Type reconstruction proves that run-time type-errors cannot occur --- provided that we define the notion of type-error rather narrowly. A similar theorem holds for Java (we think).