Assignment 7: Hindley-Milner Type Inference

Due Saturday, April 22 at 11:59PM.

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

Setup

To get the code,

  git clone linux.cs.tufts.edu:/comp/105/book-code

The code you need is in bare/nml/ml.sml.

---

Individual Problems

Working on your own, please solve Exercises 1 and 2 on page 522 of Ramsey. These exercises explore some implications of type inference.

Pair Problems

Working with a partner, please solve Exercises 18, 19 and 20 on pages 525-526 of Ramsey, and exercises S and T below.

Problem Details

18. Implementing a constraint solver. Do Exercise 18 on page 525 of Ramsey. This exercise is probably the most difficult part of the assignment. Before proceeding with type inference, make sure your solver produces the correct result on our test cases and on your test cases.

19. Implementing type inference. Do Exercise 19 on page 526 of Ramsey.

20. Adding primitives. Do Exercise 20 on page 526 of Ramsey. -

S. Test cases for the solver. Write three test cases for the constraint solver. At least two of these test cases should be constraints that have no solution. Assuming that we provide a function constraintTest : con -> answer, write your test cases as three successive calls to constraintTest. Do not define constraintTest yourself.

Here is a sample set of test cases:

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

Naturally, you will supply your own test cases, different from these.

T. Test cases for type inference. Write 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 nML. Here is a sample set of test cases:

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

Naturally, you will supply your own test cases, different from these.

---

Hints, guidelines, and testing code

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. To help you with the solver, once you have implemented solve, the following code redefines solve into a version that checks itself for sanity (ie, idempotence). It is a good idea to check that the substitution returned by your solver is idempotent before using it in your type inferencer.

    fun isStandard pairs =
        let fun distinct a' (a, tau) = a <> a' andalso not (member a' (freetyvars tau))
            fun good (prev', (a, tau)::next) =
                  List.all (distinct a) prev' andalso List.all (distinct a) next
                  andalso good ((a, tau)::prev', next)
              | good (_, []) = true
        in  good ([], pairs)
        end

    val solve =
        fn c => let val theta = solve c
                in  if isStandard theta then theta
                    else raise BugInTypeInference "non-standard substitution"
                end

In writing the type-inference code, you should refer to the typing rules of nml. With your solver in place, the type inference should be straightforward, with two exceptions: let and letrec. You can emulate the implementations for val and val-rec, but you must split the constraint into local and global portions. The splitting is covered in detail in Section 7.5.2 of the book.

Testing

The course interpreter is located in /homes/cs456/bin/nml. If your interpreter can process the initial basis and infer correct types, you are doing OK.

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))))

Pick your toughest three test cases to submit for Exercise T.

Avoid common mistakes

Here some common mistakes:

• A common mistake is to create too many fresh variables or to fail to constrain your 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 of functions that consume lists, it's sufficient to write one case for NIL and one case for PAIR.

• It's a common mistake to define a new exception and not handle it. If you define any new exceptions, make sure they are handled. It's not acceptable for your interpreter to crash with an unhandled exception just because some nano-ML code didn't type-check.

• It's a common mistake to omit the initial basis for testing and then to forget to include an initial basis in the interpreter you submit.

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

Individual Problems

You should submit two files:

• README, telling us with whom you collaborated, how long you worked, what parts you finished, and so on.
• a file meaning.nml containing your code for Exercises  1 and 2.

When you are ready, use the following command to submit your work

turnin -c cs456 -p ml-inf README meaning.nml

Pair Problems

Submit these files:

• README, telling us with whom you collaborated, how long you worked, what parts you finished, and so on.
• stest.nml, containing your answer to Exercise S
• ttest.nml, containing your answer to Exercise T
• ml.sml, containing a complete interpreter for nano-ML which includes your answers to Exercises 18, 19 and 20.

Use the command:

turnin -c cs456 -p ml-inf README ttest.nml ml.sml

Note: We must be able to compile your solution in Moscow ML by typing, e.g.,

mosmlc ml.sml

If there are errors or warnings in this step, your work will earn No Credit for functional correctness.

How your work will be evaluated

We will focus most of our evaluation on your constraint solving and type inference.