Damas-Milner, Hindley-Milner, ...
Briefly, what is the difference between Damas-Milner and Hindley-Milner typing? Are they different inferencing algorithms, or is it something like the notion of principal types is due to Damas and Milner whereas the inferencing algorithm itself is due to Hindley and Milner? It seems to me that I hear "Damas-Milner" mentioned more often in ML circles, but "Hindley-Milner" more often with regard to Haskell... -- Frank Christoph Next Solution Co. Tel: 0424-98-1811 [EMAIL PROTECTED] Fax: 0424-98-1500
Re: Damas-Milner, Hindley-Milner, ...
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).
Re: Damas-Milner, Hindley-Milner,...
christo> It seems to me that I hear "Damas-Milner" mentioned more often in ML circles, christo> but "Hindley-Milner" more often with regard to Haskell... Just briefly adding to Peter Thiemann's explanation, Damas's PhD thesis also contained a type-system for type-checking impure functional programs (references), a first version of weak polymorphism. This is probably the reason why Damas-Milner is more associated with ML rather than with pure functional programming. As a remark, the soundness proof of Damas's thesis was later found out to be flawed. I think it is still open whether his type system is sound. -- Stefan Kahrs
Re: Damas-Milner, Hindley-Milner, ...
Briefly, what is the difference between Damas-Milner and Hindley-Milner typing? None. They are different names for the same thing. The actual algorithm was discovered a number of times. Hindley wrote a history of it, which I don't have to hand. He notes that it had already been implemented on a computer in the 1950s! I believe he attributes it to Curry. It was also rediscovered by a number of others, including Jim Morris, then a PhD student at MIT. Hindley wrote down a concise description, based on logic. Milner, independently, rediscovered the algorithm, apparently not based on logic. Later, Milner and his PhD student Damas reformulated the algorithm in a much more accessible way, with the connection to logic restored. Milner's key contribution -- and very important it was, too -- was to add the syntactic form `let x=e0 in e1'. Without this, the algorithm infers principle types, but does not seriously exploit polymorphism. -- P
Re: Damas-Milner, Hindley-Milner, ...
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}
}
