Comment by siraben
5 years ago
I study type systems and programming language theory at university, and I encourage friends studying CS to at least have some understanding of type theory, such as well-known type systems (simply-typed, System F) and properties like soundness or uniqueness of typing. Why? Because as programmers we argue to death comparing the expressiveness and properties of type systems of our favorite programming languages, or we're picking up a language with features like traits or type inference. Type theory really lets you learn the heart of such features in a small, idealistic setting and specifies things rigorously and uniformly, (since languages tend to come up with their own names and examples for things like ad-hoc polymorphism, AKA typeclasses/traits/protocols/concepts), and they appear no matter the paradigm.
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)?
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?
1 reply →
> 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.
The notation is an insurmountable barrier to many.
Many introductory texts, such as Types and Programming Languages explain the notation thoroughly and start really simple, even starting from the inference rule notation, then talking about reduction of untyped arithmetic expressions, building up to the standard notation type theory.
It's interesting how calling it insurmountable both panders to and insults the people you're talking about.
Maybe a better way to describe the notation is "off-putting"?
It's not supposed to be insulting. I think the notation is more than offputting, and describing it as a barrier to entry is appropriate.
Like many kinds of formal notation it almost requires a class in a university to have it explained. The same is true of other fields dense in notation where you need to learn the conventions as much as the basics.
26 replies →
I think it's easier to do if you work up to it gradually. I read Logic by Wilfrid Hodges a few years back on a whim from some recommendation on HN. I didn't think much of the book at the time, though I recently picked up Benjamin Pierce's Types and Programming Languages. Having seen notation like that before made digesting the book much easier (along with starting with other introductory texts like Friedman and Wand's Essentials of Programming Languages).
Yeah, Essentials of Programming Languages is also another great implementation-oriented text, it has some formal things like inductive sets (which pop up in PLT anyway) and also lots of programming exercises.
Looking at java, rust or assembly i find this argument hard to swallow ;) It's really worth it to learn some sequent calculus basics to be able to read typing rules. Its mostly the same thing as a grammar, or a weird inductive type ("enum").
It shouldn't be hard to swallow. Monospaced ascii text that is (usually) unambiguous with extensive documentation is night and day from formal notation.
At least BNF grammars are legible
Look at APL, K, and J. The notation based on keywords is not a problem; the problematic notations are the ones which abuse strange characters or ideograms, because they require you to re-learn the process of reading.
The notation really isn't as bad as it originally looks, trust me. I was in the same boat recently, but after cracking open TAPL, on page 26 you basically get all the notation you need for the rest of the book.
Inference rules just transform the traditional format of
into
This format allows you to stack rules on top of each other when writing out the derivation of some term, without running out of page space.
It seems absurd to care about 'page space' when discussing computer science notation...
ah notation is such a subtle and often sad topic
when you click you never give a damn about notation but before you do it's such a drag
it's like monads