On Tuesday, 16 January 2018 at 06:26:34 UTC, thedeemon wrote:
"Practical Foundations for Programming Languages" by Robert Harper
Well, I have that one, and the title is rather misleading. Not at all practical.
electronic computers and it's still very relevant today. Anyone dabbling into compilers and programming language theory should learn the basics of type theory, proof theory and some category theory, these three are very much connected and talk about basically the same constructions from different angles (see Curry-Howard correspondence and "computational trinitarianism"). It's ridiculous how many programmers only learn about types from books on C++ or MSDN, get very vague ideas about them and never learn any actual PLT. Of course type is not a set of values, or any other set, not at all.
I don't really agree with this, empirically speaking. As many people have designed good languages without such a focus, and many have designed not very good languages with this focus...
Anyway, let's not make this too complicated, no need for a pile of tomes:
https://en.wikipedia.org/wiki/Type_theory
