3 ms·

Can someone familiar with the territory recommend a better or complementary resource of similar level of approachability? The intro here flags that the author

by abeppu 2y ago

Can someone familiar with the territory recommend a better or complementary resource of similar level of approachability? The intro here flags that the author i) is not happy with the post in its current form, ii) was resynthesized from wikipedia "without particularly putting in the effort to check my own understanding", which doesn't inspire confidence. And then when you do get into the content, stuff looks incorrect, but a non-expert reader, given the caveats in the intro, should be on the lookout for errors but isn't equipped to identify them with confidence. E.g. the very first inference rule included is described as: > if you have a variable x declared to have some polytype π, and if the monotype μ is a specialisation of π, then x can be judged to have type μ ... but I think this should be "π is a specialization of μ". Basically, I think this is the kind of material where detail matters, where errors seriously impede understanding, and a resource where the reader/learner has to be on guard second-guessing the author is a bad intro resource. But surely there are better ones out there.

nathanrf 2y ago
The quoted paragraph is correct as written. E.g. if f: ∀A, B. A -> B -> A Then we have poly type π = "∀A, B. A -> B -> A". The monotype μ = Str -> Int -> Str is a specialization of π, so we are also permitted to judge that f has type μ. The type specialization operator "looks backwards", where we write sorta "π ≤ μ" because there's a kind of "subtyping" relationship (though most HM type systems don't actually contain subtyping) - anywhere that a term of type μ is used, a term of type π can be used instead because it can be specialized to μ. I think this is a good complementary article: https://boxbase.org/entries/2018/mar/5/hindley-milner/ https://boxbase.org/entries/2018/mar/5/hindley-milner/ (it also links to three more academic sources for more context/detail)
shpongled 2y ago
"Types and Programming Languages" by Benjamin Pierce is an excellent textbook (and approachable, even to people without formal CS education) that covers type inference and introduces a lot of the nomenclature/formalism gradually.
- bbkane 2y ago
  I'm trying to go through TAPL, and maybe it's me, but I find its extremely terse and lacks a lot of examples I would find useful
  - shpongled 2y ago
    I don't know if it will be useful to you, but I worked up dependency-free parsers/type checkers in Rust for the "languages" defined in most of the chapters (at least the ones I cared about) https://github.com/lazear/types-and-programming-languages https://github.com/lazear/types-and-programming-languages
mrkeen 2y ago
This is nice and genuinely entertaining https://youtu.be/IOiZatlZtGU https://youtu.be/IOiZatlZtGU (Propositions as types by phil wadler). Its true focus is the 1-1 mapping between type systems and logic systems, but it's well worth the watch. This is good reading - it demystifies the funny typing rules in their mathematical form. https://legacy-blog.akgupta.ca/blog/2013/05/14/so-you-still-dont-understand-hindley-milner/ https://legacy-blog.akgupta.ca/blog/2013/05/14/so-you-still-... (Neither of these tell you how to implement the checker yourself though)
efnx 2y ago
It will never be finished but Stephen Diehl’s “Write you a Haskell” is great. http://dev.stephendiehl.com/fun/ http://dev.stephendiehl.com/fun/
philh 2y ago
For whatever it's worth, when I first wrote this I submitted it to /r/haskell (https://www.reddit.com/r/haskell/comments/cs7jyu/a_reckless_introduction_to_hindleymilner_type/ https://www.reddit.com/r/haskell/comments/cs7jyu/a_reckless_...) and it doesn't look like there were any corrections from that; and since then I've implemented an HM type checker and don't remember finding anything that made me think "oh, I was wrong about ...". So I'm more confident in the essay than I was at the time. But yeah, getting put on guard by those caveats doesn't seem ideal for intro material. (But if I hadn't had them and I'd gotten something wrong, that would also not have been ideal...) For writing the type checker, "write you a haskell" that someone else linked was really helpful, and so was a paper called "typing haskell in haskell": https://web.cecs.pdx.edu/~mpj/thih/thih.pdf https://web.cecs.pdx.edu/~mpj/thih/thih.pdf
almostgotcaught 2y ago
> ... but I think this should be "π is a specialization of μ". Can we reflect on how this person was so wary of reading the article for fear of being misled (instead of just reading it and afterwards reflecting/evaluating) because they were so sure it must be wrong (for whatever reasons) and it turns they themselves were wrong. This is called irony and dunning krueger.

by abeppu 2y ago

nathanrf 2y ago

The quoted paragraph is correct as written. E.g. if f: ∀A, B. A -> B -> A Then we have poly type π = "∀A, B. A -> B -> A". The monotype μ = Str -> Int -> Str is a specialization of π, so we are also permitted to judge that f has type μ. The type specialization operator "looks backwards", where we write sorta "π ≤ μ" because there's a kind of "subtyping" relationship (though most HM type systems don't actually contain subtyping) - anywhere that a term of type μ is used, a term of type π can be used instead because it can be specialized to μ. I think this is a good complementary article: https://boxbase.org/entries/2018/mar/5/hindley-milner/ https://boxbase.org/entries/2018/mar/5/hindley-milner/ (it also links to three more academic sources for more context/detail)

shpongled 2y ago

"Types and Programming Languages" by Benjamin Pierce is an excellent textbook (and approachable, even to people without formal CS education) that covers type inference and introduces a lot of the nomenclature/formalism gradually.

bbkane 2y ago
I'm trying to go through TAPL, and maybe it's me, but I find its extremely terse and lacks a lot of examples I would find useful
- shpongled 2y ago
  I don't know if it will be useful to you, but I worked up dependency-free parsers/type checkers in Rust for the "languages" defined in most of the chapters (at least the ones I cared about) https://github.com/lazear/types-and-programming-languages https://github.com/lazear/types-and-programming-languages

mrkeen 2y ago

This is nice and genuinely entertaining https://youtu.be/IOiZatlZtGU https://youtu.be/IOiZatlZtGU (Propositions as types by phil wadler). Its true focus is the 1-1 mapping between type systems and logic systems, but it's well worth the watch. This is good reading - it demystifies the funny typing rules in their mathematical form. https://legacy-blog.akgupta.ca/blog/2013/05/14/so-you-still-dont-understand-hindley-milner/ https://legacy-blog.akgupta.ca/blog/2013/05/14/so-you-still-... (Neither of these tell you how to implement the checker yourself though)

efnx 2y ago

It will never be finished but Stephen Diehl’s “Write you a Haskell” is great. http://dev.stephendiehl.com/fun/ http://dev.stephendiehl.com/fun/

philh 2y ago

For whatever it's worth, when I first wrote this I submitted it to /r/haskell (https://www.reddit.com/r/haskell/comments/cs7jyu/a_reckless_introduction_to_hindleymilner_type/ https://www.reddit.com/r/haskell/comments/cs7jyu/a_reckless_...) and it doesn't look like there were any corrections from that; and since then I've implemented an HM type checker and don't remember finding anything that made me think "oh, I was wrong about ...". So I'm more confident in the essay than I was at the time. But yeah, getting put on guard by those caveats doesn't seem ideal for intro material. (But if I hadn't had them and I'd gotten something wrong, that would also not have been ideal...) For writing the type checker, "write you a haskell" that someone else linked was really helpful, and so was a paper called "typing haskell in haskell": https://web.cecs.pdx.edu/~mpj/thih/thih.pdf https://web.cecs.pdx.edu/~mpj/thih/thih.pdf

almostgotcaught 2y ago

> ... but I think this should be "π is a specialization of μ". Can we reflect on how this person was so wary of reading the article for fear of being misled (instead of just reading it and afterwards reflecting/evaluating) because they were so sure it must be wrong (for whatever reasons) and it turns they themselves were wrong. This is called irony and dunning krueger.