If you are interested in the subject, The Implementation of Functional Programming Languages by Simon Peyton Jones is actually freely available on his Microsoft Research page : <a href="https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/" rel="nofollow">https://www.microsoft.com/en-us/research/publication/the-imp...</a><p>The book is really great. It starts with a very interesting explanation of lambda calculus and how high-level functional programming language can be tied to it. Chapters 8 and 9 were written by Peter Hancock and cover step by step how to write a polymorphic type-checker (the examples are in Miranda but it's not far from Haskell).<p>For a 1987 book, it all aged very well.
Inference is a little more involved once you add lambda abstraction and function application.<p>Recommended:<p>Christoph Hegemann: type inference from scratch: <a href="https://www.youtube.com/watch?v=ytPAlhnAKro" rel="nofollow">https://www.youtube.com/watch?v=ytPAlhnAKro</a>
Their grammar's a bit off, since they have:<p><pre><code> <bool> ::= T | F | IsZero <num>
<num> ::= O
<arith> ::= Succ <num> | Pred <num>
</code></pre>
Here `<num>` can only ever be `O`, so that's the only valid argument for `IsZero`, `Succ` and `Pred`. I would put `O` into `<arith>`, get rid of `<num>` and replace all references to it with `<arith>`.<p>That doesn't affect the actual implementation, since (as they say right after) "For simplicity, we merge all them together in a single Term."
Another educational (but more sophisticated) evaluator / typechecker in Haskell is described in "Stitch: The Sound Type-Indexed Type Checker" <a href="https://cs.brynmawr.edu/~rae/papers/2018/stitch/stitch.pdf" rel="nofollow">https://cs.brynmawr.edu/~rae/papers/2018/stitch/stitch.pdf</a>
Isn’t this a reskin of Stephen Diehl’s earlier set of blog posts? Or is this a common PL example? <a href="http://dev.stephendiehl.com/fun/004_type_systems.html" rel="nofollow">http://dev.stephendiehl.com/fun/004_type_systems.html</a>