Writing a simple evaluator and type-checker in Haskell | Hacker News Reader

Writing a simple evaluator and type-checker in Haskell

bor0.wordpress.com

126 pointsbor09 comments

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 : https://www.microsoft.com/en-us/research/publication/the-imp...

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

For a 1987 book, it all aged very well.

Self plug: Here's a Rust implementation of [one of the Virtual machines described in the book (TIM)](https://github.com/bollu/timi) I worked hard on the UI, and I hope it shows. Exploring the states through the UI gave me deep insight into how the machine works.

I once had an embarrassing post-concert-in-the-pub conversation with PH in which I confidently asserted that he didn’t understand polymorphism. “Yes I do. I wrote N chapters of a book about it”. I call BS and demand name of book. He names book. I say “but I have that book and it’s by SPJ”. “Ah” says Hank “but the chapters on polymorphism are mine!”

Hilarity.

Inference is a little more involved once you add lambda abstraction and function application.

Recommended:

Christoph Hegemann: type inference from scratch: https://www.youtube.com/watch?v=ytPAlhnAKro

Their grammar's a bit off, since they have:

    <bool>  ::= T | F | IsZero <num>
    <num>   ::= O
    <arith> ::= Succ <num> | Pred <num>

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

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" https://cs.brynmawr.edu/~rae/papers/2018/stitch/stitch.pdf

Isn’t this a reskin of Stephen Diehl’s earlier set of blog posts? Or is this a common PL example? http://dev.stephendiehl.com/fun/004_type_systems.html

It's untyped then simply typed basic imperative language, which is more or less the first few courses of programming language theory 101.

This basically summarized the first half of the programming languages course I took. Nicely done

Reply on news.ycombinator.com