Type Theory for Beginners

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.


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


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."