A tutorial on implemeting type inference?

I was wondering if anyone knew of good explanations of HM-type inference works, with an emphasis on implementation. I've found some papers using citeseer, but all of them seem to assume that the reader has a PhD in computer science and go WAY over my head (I only program as a hobby). I did some google'ing and found The Essentials of Programming Languages, but if possible, I want to avoid having to pay ~$50 just to learn one thing. After reading SICP online and after learning Haskell, I decided to write a toy Lisp interpreter with type inference, but the implementation details for the type inference escape me. What I liked about SICP was the emphasis on implementation and how they provided source code for everything. Is there a similar (freely available?) PDF that explains type inference? I apologize in advance if I accidentally posted this to the wrong forum, or if this has already been answered many times. I perused the archive a little, but I didn't find any similar requests. Although I read LtU, this is the first time I've ever posted anything.
Kind regards,

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


This is not the best place for a query like this (in my opinion) though I'm not quite sure of a better place. comp.lang.functional is certainly a possibility. Checking out the Getting Started page offers many possibilities. It, however, doesn't mention "Programming Languages: Application and Interpretation" which is probably closest to what you want.

A link to PLAI can be found

A link to PLAI can be found here.

A less canonical tutorial on (polymorphic) type inference

Perhaps you'd like the following, less canonical explanation of type
inference and type reconstruction, from simply-typed lambda-calculus
to let-polymorphism:


It was presented at the summer school FLOLAC. Chung-chieh Shan and I
wanted to emphasize type inference as abstract interpretation, and
polymorphism as inlining. The complete Haskell code for the
progression of various interpreters and type-checkers is available
from the above page.

Good tutorial

A couple of months ago I added type inference to a toy concatenative language. I just thought I'd chime in to say that Oleg's tutorial was the most useful one that I found.

Hmm. Let's give it a try.

The Wikipedia article actually isn't a bad starting point.

Your basic HM-style inference strategy works bottom-up. You design your language so that every literal has a unique type. You define some functions that are near the "bottom" of the system (add, subtract, etc.) and you define rules for those: "if add takes two ints then it return int". Basically, for each syntactic structure of the language you define a "type rule" for the gazintas and the gazoutas. These rules take the form "well, if I know the following things, then I can conclude the following other things". The type inference implementation is merely a capturing of those rules in source code. Generally you'll need some form of unification, but that's just linking things together.

For something like ML, that's about it. Some formal work is required to make sure that your type system is sound and complete, but that's not the question you seem to be asking.

Perhaps the reason that there isn't a simple tutorial is that things go downhill quickly from there. Want to define +/- over ints and floats but not strings? Great. Now you need a constraint system and a solver. Want to deal with subtypes? Now you need a solver that handles inequalities and you need to worry about contravariance. Want to do both in the same language? Now you either need a really talented psychiatrist or you need to hire Oleg. :-) Want a language that does polymorphic inference with mutability and unboxing? Now you need either the psychiatrist or Swaroop Sridhar. Aspirin is also good here. Dependent types? Really cool, but they have known to cause cranial explosions in otherwise mathematically inclined computer scientists (since his head is intact, one may infer from this that Benjamin Pierce is either not a computer scientist or not entirely human, but he's still a nice guy).

What I'm trying to get at here is that the most basic HM-style inference is pretty simple, but inference gets complicated very quickly as seemingly innocuous things get added to the language. Of course, if Joe the Language Plumber wanted to design something exactly like ML, he'ld just use ML, so each language carries its own new inference challenges. BitC is (we think) a present extreme. Of the ~30,000 lines in the BitC front end, almost 9,000 are taken up by the type inference mechanism and the constraint solver. It would probably be smaller if it weren't written in C++, but there was this reductio problem...

Lisp isn't a good candidate for HM-style type inference, for a couple of reasons. First, LISP is dynamically typed, so HM-style inference doesn't apply straightforwardly. Second, many of the things that smell like types in lisp aren't simple to describe. For example, lisp lists are heterogeneous. One way to think of this in terms of static types is that there are a whole lot of places in lisp where the constraints on what type a given symbol must be aren't constraining enough to generate a unique answer. And there really isn't anything in LISP that is mathematically analogous to sum types (unions) or product types (roughly: structures) in ML.

While BitC gives an example of one way to impose static types on LISP, it's a result achieved at considerable complexity, it's strictly static (so there are some things LISP does that it can't express) and it's inference mechanism is too complicated to serve as a learning tool. Another thing to look at if you are interested in lisp-like languages would be typed scheme, but I have no sense of how simple or complicated that inference engine might be.

One thing you might consider is looking over the Hugs implementation for haskell, which is readily available and not overwhelmingly complicated.

not overwhelmingly complicated

Great summary, shap.

Another implementation I found very instructive is Caml Light (circa 1997). Besides a relatively small type inference module, it type checks printf, and has a nice bytecode engine with documentation on its development. The ZINC paper is great.

The Book: Types and

The Book: Types and Programming Languages by Benjamin C. Pierce has the best section on HM style typechecking that I have seen. More great stuff in that book also.

Typing Haskell in Haskell

I personally found the Typing Haskell in Haskell paper useful for my discovery of HM type-inference, since a complete version of a type-checker is built progressively, in a readable and testable form (that is, in Haskell). The type-checker is built for a subset of Haskell 98 which is powerful enough to be useful as a basis for future extensions and yet understandable. I think it might be helpful to you as well.

Practical Type Inference

Since you're programming in haskell, you might find this interesting

Practical type inference for arbitrary-rank types

While the paper is about higher-rank types, it includes a tutorial on implementing HM type inference using a cool monad to keep track of unification variables (and unify them). There is an associated implementation.

Check the Nice Language Type Inference out

I believe the Nice programming language has substantial advances in type inference over basic HM implementations from ML era. (I haven't been following Haskel though. Might have the same thing.) Back when I was studying type inference there was a hard nut around higher order polymorphism that seems to have yielded ground at least practically. Google Bonniot (Nice language guy) for clues.

Luca Cardelli

I learned by reading Luca Cardelli's paper. It has working code in the appendix. It's in Modula-2, but you should be able to understand it if you know Pascal or C.