6 ms·

Writing a simple evaluator and type-checker in Haskell

126 points by bor0 8y ago

herbstein 8y ago
This basically summarized the first half of the programming languages course I took. Nicely done
chriswarbo 8y ago
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."
kornish 8y ago
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 http://dev.stephendiehl.com/fun/004_type_systems.html
- Drup 8y ago
  It's untyped then simply typed basic imperative language, which is more or less the first few courses of programming language theory 101.
brmgb 8y ago
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-implementation-of-functional-programming-languages/ 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.
- bollu 8y ago
  Self plug: Here's a Rust implementation of [one of the Virtual machines described in the book (TIM)](https://github.com/bollu/timi 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.
- colinb 8y ago
  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.
deleted 8y ago
[deleted]
platz 8y ago
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 https://www.youtube.com/watch?v=ytPAlhnAKro
danidiaz 8y ago
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 https://cs.brynmawr.edu/~rae/papers/2018/stitch/stitch.pdf

126 points by bor0 8y ago

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

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

kornish 8y ago

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 http://dev.stephendiehl.com/fun/004_type_systems.html

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

brmgb 8y ago

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-implementation-of-functional-programming-languages/ 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.

bollu 8y ago
Self plug: Here's a Rust implementation of [one of the Virtual machines described in the book (TIM)](https://github.com/bollu/timi 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.
colinb 8y ago
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.

deleted 8y ago

[deleted]

platz 8y ago

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 https://www.youtube.com/watch?v=ytPAlhnAKro

danidiaz 8y ago

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