Hacker News Reader

Comment by chestervonwinch | Hacker News Reader

What is a good an introductory text (or other resource) for learning? What's the relationship between programming language theory and type theory? Is type theory a special topic, or would it be considered a core topic in programming language theory (e.g., like integration in calculus)?

View on HN

I found the first 6 chapters of "Type Theory and Formal Proof" to be amazing for covering the beginning math behind Type Theory. The authors (Nederpelt and Geuvers) don't gloss over assumptions and they build things up step by step. I didn't study this in university but have picked up many books along the way. I'm usually quite lost within the first 10 or 20 pages until picking up Type Theory and Formal Proof. This one took me somewhere between 100 to 200 pages before getting lost. They cover the entire lambda cube.

But then I was able to re-start Thompson's "Type Theory and Functional Programming" and it was clear that I started to understand a lot of it.

If you enjoy the nostalgia of older books like me, then pick up an original copy of "Intuitionistic Type Theory" edited by Per Martin-Löf.

I love “Types and Programming Languages” by Benjamin Pierce and always recommend it for people who want to dip their toes into formal type theory. To me it’s basically the K&R for type theory.

As others have said, I also recommend Types and Programming Languages.

> What's the relationship between programming language theory and type theory?

I'd say programming language theory is more broad than type theory, for instance topics such as compilation techniques and runtime systems are more distant from type theory (though you might prove some type-theoretic thing like type preservation).

There's also a range of type theory books because it's a field that spans pure logic to programming languages, so you can find books like Type Theory and Functional Programming by Thompson that elaborate things like dependent types early on.

Thanks, that's helpful. If I was just starting out, would it be better then to start with a broader programming language theory text, rather than going straight for type theory?

Yeah it might help to see how things are implemented, for instance, even SICP can be a good foundation for this, since they also have interpreters and compilers and talk about things like "primitives" and "derived forms" and grammars.

Essentials of Programming Languages is very implementation driven and they implement a wide variety of interpreters for untyped languages, typed languages, concurrent, imperative, continuation-passing, object-oriented and more.

> What is a good an introductory text (or other resource) for learning?

The usual recommendation seems to be "Types and Programming Languages" by Benjamin C. Pierce.

Reply on news.ycombinator.com