5
$\begingroup$

I'm interested to read about type theory, but I'm quite a beginner. I know what sets are and how to work with them, but I don't have a deep understanding of set theory. I don't really understand the motivation behind type theory, other than that it was first developed to solve the problems with naive set theory.

I'm mainly interested in type theory because I heard it relates to proof theory (which I also don't understand well). I'm also not a mathematician or computer science by education.

Is there a good resource for beginners that introduces type theory, motivates it, shows how its different from set theory, why that's relevant, and shows how it can be used? I'd be satisfied if I have a thorough understanding of the general idea without understanding more advanced stuff.

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ Andrej Bauer just gave this talk to introduce type theory in one hour. If you want more, you could read (parts of) the HoTT book. $\endgroup$
    – xavierm02
    Dec 11 '17 at 22:51
  • $\begingroup$ My impression is that many introductions to type theory, especially from a more computer science perspective, are going to spend little to no time contrasting to set theory. There are plenty of reasons to study type theory without considering it as a replacement of set theory at which point there is no more reason to contrast it to set theory than there is to contrast it to ring theory. From the perspective of computation or proof theory, type theory is a perfectly natural thing to study even if you never become aware of its application to foundations. $\endgroup$
    – Derek Elkins left SE
    Dec 12 '17 at 4:45
  • $\begingroup$ @xavierm02, the hott book seems rather advanced. For example I have no idea what a weak $\infty$-groupoid or homotopy group is. On the other hand I have studied predicate logic and turing machines to some extent. I will look at the Bauer talk. $\endgroup$
    – user56834
    Dec 12 '17 at 5:22
  • $\begingroup$ @Programmer2134 As xavierm02 said, only parts of the HoTT book are relevant if you just want an overview of (one particularly influential part of) type theory. Chapter 1, most of Chapter 3, and the first four sections of Chapter 5 don't rely too heavily on the homotopy parts. In particular, the word "groupoid" only occurs once in Chapter 1 and not even as $\infty$-groupoid. Chapter 1 is basically pure type theory without any of the homotopy stuff. On the other hand, the HoTT book isn't really intended as a first introduction to type theory except perhaps for mathematicians from other fields. $\endgroup$
    – Derek Elkins left SE
    Dec 12 '17 at 9:17
3
$\begingroup$

Why has no one proposed Benjamin Pierce's Types and Programming Languages? That is a good introduction to type theory. Bob (Robert) Harper's Practical Foundations of Programming Languages is also a pretty good one.

Both of them introduce type theory from a computing perspective. If you like math better, try Rob Nederpelt and Herman Geuvers' Type Theory and Formal Proof: An Introduction. I have not taken a look at Basic Simple Type Theory by J. Roger Hindley yet, but I figure it should be good given the author (judging from the table of contents though, it looks hard).

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.