Type Theory for Beginners

Question

One of the first things one learns at university are some foundations of mathematics. This covers topics such as sets, functions between sets, relations, logic & proof, ...

I learned this stuff too. But it does not satisfy me because some things seem to be too unnatural for me. In this blog post, Dr. Shulman explains that these problems with the "standard" foundations (ZFC, ETCS) are solved by type theory.

The standard reference to learn type theory is the Homotopy Type Theory book. But this book is too complicated for me, since I am a beginner. That is why I am searching for material from which I can learn type theory. This material should be written for the same audience for which the introductions to sets, functions, ... mentioned above are written.

Answer 1

I don't have the perfect book reference for you, but here are some references that I think are worth looking at with your background. At least you could give them a try.

(1) The HoTT lectures by Robert Harper

There is a course held by Robert Harper available here. It is not easier to understand but it contains a lot of tiny hints and explanations which may help you understand parts of book. There are excellent videos, notes and exercises included.

Do not be demotivated if you don't understand everything. But again: The hints you get there pay off when you continue reading material about type theory.

(2) The book "Types and Programming Languages" by Benjamin Pierce

It describes many aspects of Type Theory from a (as the title implies) more programming language oriented perspective while covering a lot basic material, which may is exactly what you're looking for.

(3) Start learning a statically typed programming language

To turn this into a a book reference: There is a book called "Software Foundations" by Benjamin Pierce, too. It covers a very good beginner-friendly introduction to Coq, a programming language widely used in the type theory ecosystem. Bonus: It introduces type theoretic concepts on the fly including immediate applications implemented in Coq.

You could also try Agda, Haskell or Idris, too. In fact using a programming language like the one mentioned is in some sense "applying" type theory. They provide a good learning environment and most probably this will generate a lot of insights in type theory for you when combined with other learning resources.

Answer 2

To add to Robin Neumann's suggestions, you might be interested in the Oregon Programming Summer School lectures.

2015

The lectures for other years are available from the same site, and a few of those lectures are posted on youtube.

Answer 3

Last year I put together a page for exactly this purpose, outlining what I would consider the optimal path through learning Type Theory

http://purelytheoretical.com/sywtltt.html

Answer 4

Two books I'm enjoying:

1. "Types and Formal Proofs" by Nederpelt and Geuvers

2. "Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions" by Bertot and Casteran.

Like you, I have a background in set theory and logic but Type Theory has been challenging to wrap my head around, not to mention Homotopy Type Theory.

The book by Bertot and Casteran is especially good for learning applied type theory via Coq in parallel with "Software Foundations."

Answer 5

I'd suggest "Type theory and functional programming" by Simon Thompson. It's a bit older, but it gives a much gentler overview of type theory than the HoTT book. In contrast to Pierce's TAPL, it handles the full version of dependent type theory rather than the more limited theories such as F_omega. It's freely available from https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/.

Alternatively, if you want a more practical introduction to the subject then I recommend the recent book "Verified functional programming in Agda" by Aaron Stump. It is very accessible to newcomers yet it builds up to some impressive applications of type theory.