Lambda the Ultimate

The subject is ok, if I understand what it is you are asking about. I assume Pierce's book (TAPL) does not match your needs?

I found the following resources helpful for understanding type inference, in order of increasing difficulty:

1. Chapter 30 (Type Inference) of the freely available book PLAI, Programming Languages: Application and Interpretation, sketches unification-based type inference.
2. The summer course Interpreting types as abstract values presents elegant evaluators, type checkers, type reconstructors and inferencers using Haskell as a metalanguage.
3. Chapter 7 (Types) of the book EOPL, Essentials of Programming Languages.
4. Chapter 22 (Type Reconstruction) of the book TAPL, Types and Programming Languages, and the corresponding OCaml implementations recon and fullrecon.
5. Chapter 13 (Type Reconstruction) of the new book DCPL, Design Concepts in Programming Languages.
6. Selection of academic papers.

However, since the best way to learn is to do, I strongly suggest implementing type inference for a toy functional language by working through a homework assignment of a programming languages course.

I recommend these two accessible homeworks in ML, which you can both complete in less than a day:

1. PCF Interpreter (a solution) to warm up.
2. PCF Type Inference (a solution) to implement algorithm W for Hindley-Milner type inference.

These assignments are from a more advanced course:

1. Implementing MiniML

2. Polymorphic, Existential, Recursive Types (PDF)

3. Bi-Directional Typechecking (PDF)

4. Subtyping and Objects (PDF)

Well, I have some older books like Hollub's "Compiler Design in C", a nice but somewhat obscure book on writing compilers and interpreters based on Pascal implementation and so on (generally "Algol" and "Lisp" family languages). Depending on the volume, there's some theory (Hollub spends a little too much time on LL1 and LALR parsing, IIRC) and quite a bit of actual implementation code.

Now, what I'm particularly interested is a theory + practice treatment of a panoply of language type system features - type checking languages generics, constrained generics, local type inference, type level treatment of modern object oriented languages (single/multiple inheritance, multi-methods, co/contra variance, etc.), a nice treatment of HM, type inference for recursive functions, and so on and so so forth.

I'm certainly open to other suggested topics from which I will profit by addressing.

I understand that one volume might not cover all of these topics well, so I'm open to multiple suggestions.

Again, many thanks.

Scott

Benjamin Pierce's tome, Types and Programming Languages, available from an online bookseller near you. This book, frequently referred to 'round here as TAPL, is the definitive work on type theory.

A second book is Advanced Topics in Types and Programming Languages. This is also recommended; but isn't really a traditional textbook; instead it's an edited collection of papers reflecting some of the current research in the field. Pierce is the editor here, but FTMP not the author.

A third book, if you are interested in OO type theory, is Adabi and Cardelli's work A Theory of Objects; which puts much of OO programming on a rigorous formal footing.

One other interesting book to consider are Chris Date's Types and the Relational Model; albeit Date is more knowledgeable about databases than he is about type theory, and his presentation style and nomenclature is a bit strange to those coming from a FP background.

(Sorry about the broken tags in the original post; I went to edit them and found that someone had done so already)

That's the best advice I can give you. Judging from the ml-sources of TAPL it will give a very instructive introduction into terminology, logics, and current algorithms. That, might, probably will, be sufficient as an introduction to the current field.

However, (I am somewhat of a fan) Dijkstra was notorious for never reading any articles in the field since it clouded his judgements. If you start of with plain HM, I think if you analyze most of the algorithms roughly, you might actually come up with most of them yourself.

I personally understand most algorithms as simplified tactics on sequent calculi, so that is how I implement type systems [as constraint solvers]. A proof of equality is a unification tactic, generalization and specialization are rules on existential and universal quantifier introduction and elimination, equality of recursive types can be proven by co-inductive arguments, etc. You might want to read up on that too.

I personally understand most algorithms as simplified tactics on sequent calculi

I'd second this intuition. What I was doing with PrenexF (linked above) was essentially trying to make the appropriate tactics blindingly obvious!

things like Qi make that approach explicit, if i understand correctly.