40 ms·

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

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?

wcrichton 8y ago
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/dp/0262162091 https://www.amazon.com/Types-Programming-Languages-MIT-Press...
bjz_ 8y ago
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 http://www.cs.cmu.edu/~rwh/pfpl.html
etatoby 8y ago
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 https://www.youtube.com/user/DrBartosz
- bjz_ 8y ago
  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.
  - etatoby 8y ago
    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.
    - bjz_ 8y ago
      Fair enough! Yeah, I've heard good things about that series.

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?

wcrichton 8y ago

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/dp/0262162091 https://www.amazon.com/Types-Programming-Languages-MIT-Press...

bjz_ 8y ago

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 http://www.cs.cmu.edu/~rwh/pfpl.html

etatoby 8y ago

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 https://www.youtube.com/user/DrBartosz

bjz_ 8y ago
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.
- etatoby 8y ago
  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.
  - bjz_ 8y ago
    Fair enough! Yeah, I've heard good things about that series.