This is probably my favorite explanation of HM type inference, based on an analogy with region-based memory management: http://okmij.org/ftp/ML/generalization.html

That looked a bit rough in comparison but with plenty of detail. I'll add that one too. Thanks.

Well, that was enlightening actually. Thanks for posting.

Not quite sure who is downvoting that. Looks like a decent article for people who aren't like "yeah, nothing new here" after seeing the first diagram.

edit: wtf, I love you people.

Love the step by step approach connecting English and intuition to the more formal and theoretical stuff. Not ready to learn this stuff but Hindley-Milner is on my TODO list later. I can tell by first page that this will help a lot given the math looks like gibberish to me.

Note: Strange I did great in Algebra, Calculus, etc back in H.S. and college but proofs and such look gibberish. Maybe I should've taken a class with set theory or formal logic, eh? Paying for it now as I skim formal methods & FP papers...

It is a formal notation for logic that is nothing particularly like algebra. (The horizontal bar is not division, the turnstile is not a binary operation.) It's a new "syntax of symbols" that you need to learn to read in order to read logic papers.

Well, the terse notation is indeed to terse for me, and I'm not even sure what I'm trying to understand, but the explanation on the other hand is too long.

What's the null element of the set of expressions? Is (\lambda x. ) not valid and applicable?

Why is the capital gamma spammed into all the formulas, instead of adding an axiom

    foo turnstile bar

    ------------------------
    Gamma, foo turnsile bar

Γ is a shorthand for the rest of the type environment. Your suggestion would allow the type checker to invent arbitrary phantom declarations.