Hi,
Peter Thiemann writes:
> The type inference algorithm is already presented in Milner's paper
> [Milner1978] along with a soundness proof.
> Damas [DamasMilner1982] proved the completeness of the algorithm and
> the fact that the algorithm computes principal types, i.e., suppose
> the algorithm yields e : sigma. Then for each derivable typing
> judgement [] |- e : sigma' it holds that sigma' is a generic instance
> of sigma.
> Btw, some people also speak of Milner-Mycroft typing to mean ML-typing
> plus polymorphic recursion.
I always thought that the type inference algorithm, for the simply
typed lambda calculus, was first described by Curry and Feys
[curry58]. Later Hindley [hindley69] introduced the notion of
principal type, proving that the Curry and Feys algorithm inferred the
most general type. Milner [milner78] independently described a
similar algorithm, which also introduced the notion of first-order
polymorphism, often called let-polymorphism or ML style
polymorphism. Damas [damas85] later proved the completeness of
Milner's algorithm, extending the type inference system with
polymorphic references.
Best wishes
Ben
@book{curry58,
author = "H. Curry and R. Feys",
title = "Combinatory Logic",
publisher = "North-Holland",
year = "1958",
volume = "1"}
@phdthesis(damas85,
author = "Luis M. M. Damas" ,
title = "Type Assignment in Programming Languages",
school = "University of Edinburgh" ,
year = "1985" ,
month = "April",
note = "Technical report CST-33-85")
@article{hindley69,
author = "J. Roger Hindley",
title = "The Principal Type Scheme of an Object in Combinatory Logic",
journal = "Transactions of the American Mathematical Society",
year = "1969",
volume = "146",
pages = "29-60",
month = "December"}
@article{milner78,
author = "Robin Milner",
title = "A Theory of Type Polymorphism in Programming",
journal = "Journal of Computer and System Sciences",
year = "1978",
month = "August",
volume = "17",
pages = "348-375"}
--------
Benedict R. Gaster.
Languages and Programming Group, University of Nottingham.
A thing of beauty is a joy forever -- John Keats (1795--1821).
