28
$\begingroup$

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

$\endgroup$
28
$\begingroup$

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.

$\endgroup$
  • 10
    $\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$ – Martin Berger Aug 21 '14 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$ – Huck Bennett Aug 21 '14 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$ – Steven Shaw Aug 25 '14 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$ – Martin Berger Aug 27 '14 at 15:25
10
$\begingroup$

Barendregts Lambda Calculi with Types is more advanced, but it covers some important topics in the "classical" theory of types.

$\endgroup$
9
$\begingroup$

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

$\endgroup$
5
$\begingroup$

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.

$\endgroup$
  • 6
    $\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$ – Nikolaj-K Aug 21 '14 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$ – Martin Berger Aug 22 '14 at 12:13
  • 1
    $\begingroup$ Not introductory :) $\endgroup$ – Steven Shaw Aug 22 '14 at 22:09
4
$\begingroup$

Another nice book that weaves type theory with programming in a functional language is Didier Remy's Using, Understanding, and Unraveling the OCaml Language.

$\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.