Implementing uML: Hindley-Milner Type Inference

In this assignment you will implement Hindley-Milner type inference, which represents the current ``best practice'' for flexible static typing. The assignment has two purposes:

• To help you develop a deep understanding of type inference
• To help you continue to build your ML programming skills

Two problems to do by yourself

Six problems to do with a partner

U. Test cases for unification.
Submit three test cases for unification. At least two of these test cases should be for types that have no unifier. Assuming that we provide a function unifyTest : ty * ty -> answer, put your test cases in file utest.sml as three successive calls to unifyTest. Do not define unifyTest yourself.

Here is a sample utest.sml file:

val _ = unifyTest (TYVAR "a", TYVAR "b")
val _ = unifyTest (CONAPP (TYCON "list", [TYVAR "a"]), TYCON "int")
val _ = unifyTest (TYCON "bool", TYCON "int")

T. Test cases for type inference.
Submit three test cases for type inference. At least two of these test cases should be for terms that fail to type check. Each test case should be a definition written in uML. Put your test cases in a file ttest.uml. Here is a sample ttest.uml file:

(val weird (lambda (x y z) (cons x y z)))
(+ 1 #t)
(lambda (x) (cons x x))

For the remaining problems, here are some additional remarks and suggestions.

• Implement unification
  Complete Exercise 6 on page 287 of Ramsey and Kamin. Be sure your unifier produces the correct result on our three test cases and also on your three test cases.
  This problem is probably the most difficult part of the assignment, and you are well advised to show your unification code to the course staff before proceeding with type inference.

  Hints: Read the Unification section on pages 272–273. Be careful when you unify a list that you use all the information you compute, and that you use it as soon as possible. You'll be passing subsitutions like mad. It may be easiest to unify the tails first, then the heads. For ideas, you might want to look at the typesof function on page 276 of Ramsey and Kamin.

• Plan for type inference
  Complete Exercise 5 on page 287 of Ramsey and Kamin. Put your answer in file rules.pdf.

• Implement type inference
  Complete Exercise 8 in Ramsey and Kamin.

• New primitives
  Complete Exercise 9 in Ramsey and Kamin.

This is one assignment where it pays to run a lot of tests, of both good and bad definitions. The most effective test of your algorithm is not that it properly assign types to correct terms, but that it reject ill-typed terms. This assignment is your best chance to earn the large bonuses available by finding bugs in the instructor's code. I have posted a functional topological sort that makes an interesting test case.

Incidentally, if you call your interpreter ml.sml, you can build a standalone version in a.out by running mosmlc ml.sml or a faster version in ml by running mlton -output ml ml.sml.

Extra Credit

Type soundness (very difficult).

Prove that the uML interpreter never raises BugInTypeInference. That is, prove that well-typed uML programs don't go wrong.

Testing

The real test of your interpreter is that it should reject incorrect definitions. You should prepare a dozen or so definitions that should not type check, and make sure they don't. For example:

(val bad (lambda (x) (cons x x)))
(val bad (lambda (x) (cdr (pair x x))))

Avoid common mistakes

• A surprisingly common mistake is to fail to apply a substitution, as shown in the textbook (the example in the section on unification). Depending on how you organize your unifier, you will have more then on opportunity to make this mistake. And you can make the same mistake in type inference itself.

• Another common mistake is to create too many fresh variables.

• Another surprisingly common mistake is to include redundant cases in the code for inferring the type of a list literal. As is almost always true with functions that consume lists, it's sufficient to write one case for NIL and one case for PAIR.

There are also some common assumptions which are mistaken:

• It is a mistake to assume that an element of a literal list always has a monomorphic type.
• It is a mistake to assume that begin is never empty.

What to submit

For your work with a partner, run submit105-ml-inf-pair to submit these files:

Your solutions are going to be evaluated automatically. We must be able to compile your solution in Moscow ML by typing, e.g.,

mosmlc ml.sml