Lambda the Ultimate

Hi,
I am looking everywhere for the proofs of the correctness and completeness of the Hindley-Milner type inference algorithm.

I could only find this short paper,
Principal type-schemes for functional program, by Damas and Milner, which gives only sketches of the proofs, and inform the reader that the detailed proofs are in Damas's Ph.D. thesis, titled Type Assignment in Programming Language, that I cannot find anywhere.

I would be grateful if anyone could point me to these proofs.

R.K.

I should point out that saying it's all syntax in the end isn't the same as saying that languages are syntactic sugar. The term "Syntactic sugar" is often misused. It is a technical term, with precise meaning ;-)

Personally, I find this sort of humour bothering: Oh, absolutely. And, you know, honestly, first of all, let's give credit where credit is due. I am not inventing anything completely new here. It's all based on this thing called lambda expressions or lambda calculus or whatever, which has existed in the functional programming space for decades. But somehow, that has never really seen the light of day in a mainstream programming language.

Imagine a doctor (GP) talking about the Avian flu: "There's something called mutations or whatever, which has existed in biology for decades. But somehow, that has never really seen the light of day in general medical practice."

It's quite legitimate to mention that some of these ideas, while not original, were indeed not to be found in "mainstream languages" (even though, one could argue that C# isn't the first to try to do something about it). But why the dismissive "or whatver"? LC is part of the science of programming (and of CS in general), and to me that sounded like trying to make Philistines happy. I think all of us can try to raise the level of discussion in the field.

It's an interesting interview nonetheless, and Anders always sounds like a nice and reasonable person.

An article by Bruce Tate about a few 'technologies' that may challenge Java. The first one is 'Dynamic Languages.' He uses one example where two variables are operated upon and assigned in a single line: x1, x2 = x2, x1+x2, in contrast to Java approach which takes more lines. He also says "With Ruby, types are dynamic, so you don't have to declare them." If I am not mistaken, both can be done (and are done) in statically typed language. 'Single line, multiple assignments' could be done using tuples and type inference allows one to avoid declaring types.

He also mentions continuation servers, meta programming and convention over configuration. As an aside, while describing continuations, he writes: "Continuations are language constructs that let you quickly store the state of a thread, and execute that thread later." As far as I know, continuation simply allow an explicit return address of a function/procedure to be provided (rather than the default).