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
