Frank> Briefly, what is the difference between Damas-Milner and Hindley-Milner
Frank> typing? Are they different inferencing algorithms, or is it something like
Frank> the notion of principal types is due to Damas and Milner whereas the
Frank> inferencing algorithm itself is due to Hindley and Milner?
Frank> It seems to me that I hear "Damas-Milner" mentioned more often in ML
circles,
Frank> but "Hindley-Milner" more often with regard to Haskell...
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.
-Peter
@ARTICLE{Milner1978,
AUTHOR = {Robin Milner},
TITLE = {A Theory of Type Polymorphism in Programming},
JOURNAL = jcss,
YEAR = 1978,
VOLUME = {17},
PAGES = {348-375}
}
@INPROCEEDINGS{DamasMilner1982,
CROSSREF = {POPL1982},
AUTHOR = {Luis Damas and Robin Milner},
TITLE = {Principal Type-Schemes for Functional Programs},
YEAR = 1982,
PAGES = {207-212}
}
