Hacker News Reader

Comment by DoofusOfDeath | Hacker News Reader

I can't tell if my question is off-topic or not, but..

Can anyone recommend a book (or whatever) that introduces the aspects of type theory relevant to a would-be language designer?

View on HN

Strongly recommend Types and Programming Languages [1]. I think it's the most useful + accessible book on type theory out there.

[1] https://www.amazon.com/Types-Programming-Languages-MIT-Press...

I hear that Practical Foundations of Programming Languages by Robert Harper[0] is highly recommended. I have Types and Programming Languages, but found it a little dry to be honest. I do use it as a reference manual in my work though.

[0]: http://www.cs.cmu.edu/~rwh/pfpl.html

I recommend these introductory lectures to Category Theory. I'm going through them right now.

I assume you know some math/set theory and some Haskell, otherwise you may want to work though some of the chapters in Real World Haskell first.

Oh and put the videos at 1.25× or 1.5× otherwise you will fall asleep.

https://www.youtube.com/user/DrBartosz

Don't get me wrong - CT is a super handy thing to learn, and it pops up a ton when thinking about any software, including type checkers and compilers, but the OP was specifically asking about type theory and programming language implementation. Yes, you can express lots of category theory in terms of type theory (the dream is to implement all of it in terms of TT so that we can mechanise it), but it won't be the best use of your time if you want to build a type system.

I probably phrased my suggestion wrong. Yes, it's not central to OP's enquiry. But I did find a basic understanding of CT to help a lot when reasoning about types, and that lecture series gives just that in a relatively simple way.

Fair enough! Yeah, I've heard good things about that series.

Reply on news.ycombinator.com