So you still don't understand Hindley-Milner? (2013)(akgupta.ca)
akgupta.ca
So you still don't understand Hindley-Milner? (2013)
http://akgupta.ca/blog/2013/05/14/so-you-still-dont-understand-hindley-milner/
5 comments
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.
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...
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?
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.