I spent a very geeky Saturday reading about different kinds of logic programming languages, which somehow got me interested in learning more about type theory. After spending some time gathering introductory materials on my own I posted a question on /r/compsci asking for suggestions redditors might have on the subject. This page is both a collection of the suggested materials and general observations from /r/compsci denizens and some of my own musings on the subject; basically a learning diary of sorts. What that means is that
Under no circumstances should you think I actually know what I'm talking about. I don't
all corrections and further suggestions are more than welcome.
It was suggested that it would be good to have some knowledge of at least the following areas before delving into type theory:
The connection between predicate calculus and lambda calculus was surprising, to say the least: it turns out that you can do computations using systems of formal logic. Take for example a function of type a
b which takes things of type a and gives you things of type b. When you think about it, succesfully applying that function proves that you can get something of type b from type a, so the type of the function is actually a proposition. The awesomeness doesn't end there: according to something called the Curry-Howard correspondence (C-H from now on), not only do types correspond to propositions, but whole systems of logic correspond to different lambda calculi. The upshot of this is that all programming language concepts have corresponding logical concepts: types correspond to propositions, recursion to induction and so on.
Structural induction seems to tie into C-H, since it can be used to prove some property P for all elements of a recursively defined type.
Out of all the prerequisites, operational semantics was the only one that was completely alien to me so I'll just quote Wikipedia's handy definition: "The operational semantics for a programming language describes how a valid program is interpreted as sequences of computational steps". Its usage seems to be related to type checking: operational semantics can apparently be used to guarantee that an expression's type doesn't change during runtime. Couple this with strong typing and proper compile-time type checking and you have a language that shouldn't raise runtime type errors.
Since Wikipedia articles aren't always the best way to start learning something new, I dug up some introductory materials from various universities and institutions:
MIT OCW's Mathematics for Computer Science contains introductions to (among other things) first-order logic and structural induction on recursive data types. Sadly nothing on lambda calculus
Introduction to Lambda Calculus from Chalmers
An Introduction to Operational Semantics from Indian Institute of Technology Delhi
First order logic lecture slides from Berkeley (PPT file so link is to Google Docs viewer)
Note that some of the books and materials on type theory also cover the prerequisites.
So far all I have regarding type theory is a few links. More to come once I actually get here.
The book Types and Programming Languages (commonly referred to as TaPL) by Benjamin Pierce is apparently the book when it comes to practical applications of type theory. I was told it also covers most of the prerequisite subjects
The aptly named sequel to TaPL, Advanced Topics in Types and Programming Languages (also by Pierce)
The book Type Theory & Functional Programming which is freely available online
Lectures on the Curry-Howard Isomorphism (also available online) was suggested as good theoretical work, in comparison to the more practical approach that TaPL takes. Also contains introductions to lambda calculus and intuitionistic logic
The online book Implementing Mathematics with The Nuprl Proof Development System happens to contain an introduction to type theory. Even though it's not directly related, it is an interesting read in its own right
University of Oregon's Logic, Languages, Compilation and Verification summer school course with videos of several lectures on the subject. Since this is a complete course it covers a fair amount of the prerequisites as well