implementing type inference

Question

well I see some interesting discussions here about static vs. dynamic typing I generally prefer static typing, due to compile type checking, better documented code,etc. However I do agree that they do clutter up the code if done the way Java does it, for example.

so Im about to start building a language of my own and type inference is one of the things that I want to implement, in a functional style language... I do understand that it is a big subject, and Im not trying to create something that has not been done before, just basic inferencing...

any pointers on what to read up that will help me with this? preferably something more pragmatic/practical as oppose to more theoretical category theory/type theory texts. If there's a implementation discussion text out here, with data structures/algorithms, that would just be lovely

much appreciated

Answer 1

Lambda the Ultimate, starting here.

Answer 2

Types and Programming Languages by Benjamin C. Pierce

Answer 3

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)

Answer 4

It's unfortunate that much of the literature on the subject is very dense. I too was in your shoes. I got my first introduction to the subject from Programming Languages: Applications and Interpretation

http://www.plai.org/

I'll try to summarize the abstract idea followed by details that I did not find immediately obvious. First, type inference can be thought of generating and then solving constraints. To generate constraints, you recurse through the syntax tree and generate one or more constraints on each node. For example, if the node is a '+' operator, the operands and the results must all be numbers. A node that applies a function has the same type as the result of the function, and so on.

For a language without 'let', you can blindly solve the above constraints by substitution. For example:

(if (= 1 2) 
    1 
    2)

here, we can say that the condition of the if statement must be boolean, and that the type of the if statement is the same as the type of its "then" and "else" clauses. Since we know 1 and 2 are numbers, by substitution, we know the "if" statement is a number.

Where things get nasty, and what I couldn't understand for a while, is dealing with let:

(let ((id (lambda (x) x)))
    (id id))

Here, we've bound 'id' to a function that returns whatever you've passed in, otherwise known as the identity function. The problem is the type of the function's parameter 'x' is different on each usage of id. The second 'id' is a function from a->a, where a can be anything. The first is from (a->a)->(a->a) This is known as let-polymorphism. The key is to solve constraints in a particular order: first solve constraints for the definition of 'id'. This will be a->a. Then fresh, separate copies of the type of id can be substituted into the constraints for each place 'id' is used, for example a2->a2 and a3->a3.

That wasn't readily explained in online resources. They'll mention algorithm W or M but not how they work in terms of solving constraints, or why it doesn't barf on let-polymorphism: each of those algorithms enforce an ordering on solving the constraints.

I found this resource extremely helpful to tie Algorithm W, M, and the general concept of constraint generation and solving all together. It's a little dense, but better than many:

http://www.cs.uu.nl/research/techreps/repo/CS-2002/2002-031.pdf

Many of the other papers there are nice too:

http://people.cs.uu.nl/bastiaan/papers.html

I hope that helps clarify a somewhat murky world.

Answer 5

thanks guys I have my hands full here with all the reading material you've thrown my way. very juicy. Paul, thanks for practical info, I will dissect and you can count on me either continuing this thread when Im more knowledgeable/have more questions, or starting another thread on a related topics

much thanks

Answer 6

Take a look at this:

http://fsharpcode.blogspot.com/2010/08/hindley-milner-type-inference-sample.html