Ask HN: any type theory book recommendation?

[smikhanov]

After spending some time with Haskell, I was considering diving into some more type theory. Any recommendation for the good type theory book?

I know about Pierce's "Types and Programming Languages" and "Advanced Topics in Types and Programming Languages" but would like to learn whether there are any comparable alternatives.

Thanks in advance!

[alexk7]

I didn't read any type theory book but I'm interested in the subject. I think I will buy Pierce's "Types and Programming Languages" based on the recommendations on this thread: http://lambda-the-ultimate.org/node/492

[smikhanov → alexk7]

Really great thread, thanks for pointing that out

[tomstuart]

I strongly recommend "Proofs and Types" (http://www.PaulTaylor.EU/stable/Proofs%2BTypes.html), which has the added advantage of being free.

[smikhanov → tomstuart]

Thanks, added to the bookmarks. Alongside with the one I found earlier http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf, this book seem to cover not the type theory per se, but the mathematics that make its foundations. This is great, though not exactly what I'm looking for.

[tomstuart → smikhanov]

It depends what you mean by "type theory", but you're right. See Pierce for a more practical introduction. "Proofs and Types" is more fundamental and focuses on the interplay between the operational semantics of the underlying language and the structure of its type system (read as proofs of properties of programs written in the language).

[steveklabnik]

I personally read "Category Theory for Computer Scientists." - http://www.amazon.com/Category-Computer-Scientists-Foundatio...

It was pretty rough. Reactions by page:

1-2 "This is pretty easy." 3-5 "Okay, I can see how this is getting harder..." 6-... "My mind is blown."

The real difficulty is that it dives into mathematical notation that I'm not used to reading fairly quickly. I'm still slogging away at it in my spare time.

[chriseidhof]

I've only read Pierce, and it's good. As an alternative, you could look at dependent types if you want to know more about types. Dependent types are like GADTs on steroids. A good place to start is Agda (http://wiki.portal.chalmers.se/agda/) or Idris (http://www.cs.st-andrews.ac.uk/~eb/Idris/).

[ekiru]

The resident type theorist at a college I was considering attended recommended Luca Cardelli to me when I asked about good introductory texts: http://www.eecs.umich.edu/~bchandra/courses/papers/Cardelli_...

[tophercyll]

Chapter 7 of Essentials of Programming Languages (EoPL) has a nice introduction to some basic topics including type checking and type inference.

It's a nice gradual introduction, and help me get started with TaPL (although I wish I could say I'd made much progress).

[gtani]

This study groups is using the out of print Barr/wells, which I couldn't find for purchase

http://groups.google.com/group/bacat/topics?start=

[pushout → gtani]

You should purchase the third edition of Barr & Wells directly from the publisher. Centre de Recherches Mathematiques. http://www.crm.umontreal.ca/pub/Collections/desc/PM023.html

[enum]

"Practical Foundations of Programming Languages", available online:

http://www.cs.cmu.edu/~rwh/plbook/book.pdf

[leif]

I believe http://www.cs.nott.ac.uk/~gmh/cat.html was on HN sometime in the last two weeks. It's a very very good introduction to the underlying mathematical structures Haskell uses for its type system.

[stralep]

Programming in Martin-Löf's Type Theory http://www.cs.chalmers.se/Cs/Research/Logic/book/

I'm reading it from time to time. Useful for me.