Grow Your Own Type System

github.com

105 points·wtetzner··8 comments

Open articleView on HN

This looks like the beginning of a good suggestion:

"The book that I really, really want: Lisp in Small Pieces, but for type theory"

https://twitter.com/d_christiansen/status/573767527081316354

I want that book too.

Doesn't "Types and Programming Language" by B. Pierce fits this description? I did not read LiSP, though.

This is really cool. It's surprisingly hard to find good examples of how to implement type inference.

If I remember right, TAPL (Types and Programming Languages by Benjamin Pierce) contains implementations for nearly everything that it talks about. So you can find another implementation of Hindley-Milner there.

I don't think it includes row typing though.

Yes, there are implementations for many of the type systems in the book. :)

https://www.cis.upenn.edu/~bcpierce/tapl/checkers/

The code is pretty elegant. I think it's intended to be clear enough for students in his classes to modify.

I think PLAI gets into it, but I've not read it. http://cs.brown.edu/courses/cs173/2012/book/

One of the issues I've found with the TAPL examples and Grow-Your-Own-Type-System implementations is the lack of explicit, top-level type definitions. I know whole-program type inference is great and all, and ML programmers love to show it off, but it makes everything much harder to follow and understand.

That said, they are still very useful, and I'm thankful that the author published them!

That's a fair point (the repo doesn't even have .mli files, it looks like). However, the author has at least gone for somewhat-helpful binding names, as opposed to the single-letters-are-cool which all too common in OCaml codebases.

Reply on news.ycombinator.com