So you still don't understand Hindley-Milner? (2013)

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

Well, that was enlightening actually. Thanks for posting.

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...

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