I'm recently studying Haskell and programming languages. Could someone recommend some books on type theory?
$\begingroup$
$\endgroup$
1
-
5$\begingroup$ You might be interested in my collection of resources on Type Theory $\endgroup$– Steven ShawCommented Aug 25, 2014 at 1:39
Add a comment
|
5 Answers
$\begingroup$
$\endgroup$
4
Software Foundations 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. There is also Simon Thompson's Type Theory and Functional Programming and Girard's Proofs and Types.
-
14$\begingroup$ 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. $\endgroup$ Commented Aug 21, 2014 at 15:52
-
4$\begingroup$ Yes, TAPL is the book. There's also Pierce's "Advanced Topics in Types and Programming Languages" as a follow-up. $\endgroup$ Commented Aug 21, 2014 at 20:57
-
$\begingroup$ @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? $\endgroup$ Commented Aug 25, 2014 at 3:42
-
1$\begingroup$ @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. $\endgroup$ Commented Aug 27, 2014 at 15:25
$\begingroup$
$\endgroup$
1
Barendregts Lambda Calculi with Types is more advanced, but it covers some important topics in the "classical" theory of types.
-
$\begingroup$ Thanks @cody, I'd neglected to mention Barendregt in my collection of resources on the subject. $\endgroup$ Commented Aug 25, 2014 at 1:58
$\begingroup$
$\endgroup$
Robert Harper's book Practical Foundations for Programming Languages (available as a draft online: http://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf) is a somewhat more intense alternative to Types and Programming Languages.
$\begingroup$
$\endgroup$
3
It's more about mathematical foundations and less about computer science, but the book Homotopy Type Theory: Univalent Foundations of Mathematics is available for free in pdf form under a CC license.
answered Aug 21, 2014 at 19:16
-
7$\begingroup$ 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. :) $\endgroup$ Commented Aug 21, 2014 at 22:10
-
1$\begingroup$ 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 first. Agda is (simplifying a bit) Haskell with dependent types, and has been used to formalise Hott. $\endgroup$ Commented Aug 22, 2014 at 12:13
-
1
$\begingroup$
$\endgroup$
Another nice book that weaves type theory with programming in a functional language is Didier Remy's Using, Understanding, and Unraveling the OCaml Language.
