Prerequisites for understanding Type Theory

Question

I am a computer scientist, and I am currently trying to understand the basis of programming languages (e.g. Haskell and Coq) in the mathematical foundations. I started by reading Types and Programming Languages by Benjamin C. Pierce but I find it hard to grasp even the basics like preorder, partial and full ordered sets. What prerequisites do I need to smoothly read through such material? Do you suggest books / online courses for that matter? Many thanks.

Answer 1

It looks like you need to widen your perspective of mathematics. For type theory, Martin-Löf's original writings are still an excellent place to start.

Answer 2

It's true that TaPL assumes that readers are basically already familiar with some of those mathematical concepts - the presentation in its Chapter 2 functions more as a reminder and an establishment of notation than it does as an introduction to the ideas. Additionally, much of the rest of the text depends on a familiarity with how mathematics is commonly presented and how proofs tend to go.

I think what you are looking for is what university CS departments commonly place in a course on "mathematical foundations" or something with that kind of name. That would have an emphasis on discrete structures, proof techniques such as induction, and some of the order-theoretic concepts you mention - selected for their utility in CS theory.

As a starting point, I'd suggest Ed Scheinerman's text Mathematics: A Discrete Introduction, because it is very expansive in its presentation of these topics. You get a lot of pictures and examples and exercises to help. But there are many other books of this kind, so if that one doesn't chime with you or you find it difficult to obtain, it's just as well to go with what makes sense for you.

TaPL also recommends (the first sections of) Halmos's Naive Set Theory, Davey and Priestley's Introduction to Lattices and Order, and Winskel's The Formal Semantics of Programming Languages. All of these are very good books, which do also go quite a bit beyond the basics; something like Haggarty's Discrete Mathematics for Computing might be a bit gentler as it spends more time connecting the ideas to their CS applications.

Additionally, as you progress through the text, you might like to pick up some material on formal programming language semantics, especially operational semantics. That is not a strict prerequisite for TaPL but you would find a lot of the same ideas in play, which might help to reinforce some of the concepts in that text. Glynn Winskel's book is a great example.