<p>Barendregts <a href="http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf">Lambda Calculi with Types</a> is more advanced, but it covers some important topics in the "classical" theory of types.</p>

CC BY-SA 3.0
2014-08-25T01:58:14.170Z
Thanks @cody, I'd neglected to mention Barendregt in my [collection of resources on the subject](http://github.com/steshaw/plt-study).
Steven Shaw
CC BY-SA 3.0
2014-08-23T17:20:00.683Z
2014-08-23T17:20:00.683Z
cody
<p>Robert Harper's book Practical Foundations for Programming Languages (available as a draft online: <a href="http://www.cs.cmu.edu/%7Erwh/pfpl/2nded.pdf" rel="nofollow noreferrer">http://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf</a>) is a somewhat more intense alternative to Types and Programming Languages.</p>

CC BY-SA 4.0
2014-11-20T20:20:24.407Z
2021-01-01T15:46:48.903Z
2021-01-01T15:46:48.903Z
Chris Martens
<p>It's more about mathematical foundations and less about computer science, but the book <a href="http://homotopytypetheory.org/book/" rel="noreferrer">Homotopy Type Theory: Univalent Foundations of Mathematics</a> is available for free in pdf form under a CC license.</p>

CC BY-SA 3.0
2014-08-21T22:10:56.540Z
I like the topic and the book, but clearly, it's not like the it doesn't assume you're familiar with the rules of lambda abstractions, reductions etc. already. The OP, coming from using Haskell and now being curious about type theory, will be baffled by the interpretation of homotopy theory via identity types, 80 pages in. :)
Nikolaj-K
CC BY-SA 3.0
2014-08-22T12:13:13.047Z
I agree with @NikolajK that the Hott book is too advanced for a type-theory beginner. A good route for a Haskell programmer is to learn [Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php) first. Agda is (simplifying a bit) Haskell with dependent types, and has been used to formalise Hott.
Martin Berger
CC BY-SA 3.0
2014-08-22T22:09:24.220Z
Not introductory :)
Steven Shaw
CC BY-SA 3.0
2014-08-21T19:16:37.613Z
2014-08-21T19:16:37.613Z
David Eppstein
<p>Another nice book that weaves type theory with programming in a functional language is Didier Remy's <a href="http://gallium.inria.fr/~remy/cours/appsem/ocaml.pdf" rel="nofollow">Using, Understanding, and Unraveling the OCaml Language</a>.</p>

CC BY-SA 3.0
2014-08-27T05:27:35.327Z
2014-08-27T05:27:35.327Z
Radu GRIGore
<p><a href="http://www.cis.upenn.edu/~bcpierce/sf/current/index.html">Software Foundations</a> by Benjamin C. Pierce would be a good place to start. It would be a make a good precursor to his <a href="http://www.cis.upenn.edu/~bcpierce/tapl/">Types and Programming Languages</a>. There is also Simon Thompson's <a href="https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/">Type Theory and Functional Programming</a> and Girard's <a href="http://www.paultaylor.eu/stable/Proofs+Types.html">Proofs and Types</a>.</p>

CC BY-SA 3.0
2014-08-21T15:52:46.843Z
I'd suggest to ready Peirce's *Type and Programming Languages* first before *Software foundations* which is more advanced. For somebody wanting to start slow, something like *Lambda-Calculus and Combinators* by Hindley and Seldin is a gentle introduction.
Martin Berger
CC BY-SA 3.0
2014-08-21T20:57:14.277Z
Yes, TAPL is *the* book. There's also Pierce's "Advanced Topics in Types and Programming Languages" as a follow-up.
Huck Bennett
CC BY-SA 3.0
2014-08-25T03:42:38.670Z
@MartinBerger, I took a look at the table of contents for _Lambda-Calculus and Combinators_ and it seems a little daunting. Are you sure it's more introductory than TAPL or SF?
Steven Shaw
CC BY-SA 3.0
2014-08-27T15:25:35.673Z
@StevenShaw Hindley/Seldin starts with the very basics and proceeds really slowly, but comprehensively. The type theoretical part doesn't do anything fancy. Maybe Hindley's _Basic Simple Type Theory_ is also appropriate. I've never held it in my hands though.
Martin Berger
CC BY-SA 3.0
2014-08-21T11:32:19.530Z
2014-08-25T01:51:07.763Z
2014-08-25T01:51:07.763Z
Steven Shaw
<p>I'm recently studying Haskell and programming languages.  Could someone recommend some books on type theory?</p>

CC BY-SA 3.0
2014-08-25T01:39:31.397Z
You might be interested in my [collection of resources on Type Theory](https://github.com/steshaw/plt-study#type-theory)
Steven Shaw
<soft-question><pl.programming-languages><type-theory>
What are some good introductory books on type theory?
qazwsx
# What are some good introductory books on type theory?

(Asked by: username_0 on 2014-08-21)

I'm recently studying Haskell and programming languages. Could someone recommend some books on type theory?

**Tags:** soft-question, pl.programming-languages, type-theory
> **Comments:**
> **username_1**: You might be interested in my [collection of resources on Type Theory](https://github.com/steshaw/plt-study#type-theory)  

---

## 5 answers

### Answer by username_1 on 2014-08-21. Score: 38 | Accepted answer

[Software Foundations](http://www.cis.upenn.edu/~bcpierce/sf/current/index.html) by Benjamin C. Pierce would be a good place to start. It would be a make a good precursor to his [Types and Programming Languages](http://www.cis.upenn.edu/~bcpierce/tapl/). There is also Simon Thompson's [Type Theory and Functional Programming](https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/) and Girard's [Proofs and Types](http://www.paultaylor.eu/stable/Proofs+Types.html).

> **Comments:**
> **username_6**: I'd suggest to ready Peirce's *Type and Programming Languages* first before *Software foundations* which is more advanced. For somebody wanting to start slow, something like *Lambda-Calculus and Combinators* by Hindley and Seldin is a gentle introduction.  
> **username_8**: Yes, TAPL is *the* book. There's also Pierce's "Advanced Topics in Types and Programming Languages" as a follow-up.  
> **username_1**: @MartinBerger, I took a look at the table of contents for _Lambda-Calculus and Combinators_ and it seems a little daunting. Are you sure it's more introductory than TAPL or SF?  
> **username_6**: @StevenShaw Hindley/Seldin starts with the very basics and proceeds really slowly, but comprehensively. The type theoretical part doesn't do anything fancy. Maybe Hindley's _Basic Simple Type Theory_ is also appropriate. I've never held it in my hands though.  

---

### Answer by username_2 on 2014-08-23. Score: 11

Barendregts [Lambda Calculi with Types](http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf) is more advanced, but it covers some important topics in the "classical" theory of types.

> **Comments:**
> **username_1**: Thanks @cody, I'd neglected to mention Barendregt in my [collection of resources on the subject](http://github.com/steshaw/plt-study).  

---

### Answer by username_3 on 2014-11-20. Score: 9

Robert Harper's book Practical Foundations for Programming Languages (available as a draft online: [http://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf](http://www.cs.cmu.edu/%7Erwh/pfpl/2nded.pdf)) is a somewhat more intense alternative to Types and Programming Languages.


---

### Answer by username_4 on 2014-08-21. Score: 5

It's more about mathematical foundations and less about computer science, but the book [Homotopy Type Theory: Univalent Foundations of Mathematics](http://homotopytypetheory.org/book/) is available for free in pdf form under a CC license.

> **Comments:**
> **username_5**: I like the topic and the book, but clearly, it's not like the it doesn't assume you're familiar with the rules of lambda abstractions, reductions etc. already. The OP, coming from using Haskell and now being curious about type theory, will be baffled by the interpretation of homotopy theory via identity types, 80 pages in. :)  
> **username_6**: I agree with @NikolajK that the Hott book is too advanced for a type-theory beginner. A good route for a Haskell programmer is to learn [Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php) first. Agda is (simplifying a bit) Haskell with dependent types, and has been used to formalise Hott.  
> **username_1**: Not introductory :)  

---

### Answer by username_7 on 2014-08-27. Score: 4

Another nice book that weaves type theory with programming in a functional language is Didier Remy's [Using, Understanding, and Unraveling the OCaml Language](http://gallium.inria.fr/~remy/cours/appsem/ocaml.pdf).


---

