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
