Implementing nML: 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

Getting the code

  git clone linux.cs.tufts.edu:/comp/105/build-prove-compare

Two exercises to do by yourself (10%)

Five exercises to do with a partner (90%)

S. Test cases for the solver.
Submit 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, put your test cases in file stest.sml as three successive calls to constraintTest. Do not define constraintTest yourself.

Here is a sample stest.sml file:

val _ = constraintTest (TYVAR "a" ~ TYVAR "b")
val _ = constraintTest (CONAPP (TYCON "list", [TYVAR "a"]) ~ TYCON "int")
val _ = constraintTest (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 nML. Put your test cases in a file ttest.nml. Here is a sample ttest.nml file:

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

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

• Implement a constraint solver
  Complete Exercise 15 on page 350 of Ramsey. Be sure your solver produces the correct result on our three test cases and also on your three test cases.
  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. You may want to show your solver code to the course staff.

• Implement type inference
  Complete Exercise 16 on page 350 Ramsey.

• New primitives
  Complete Exercise 17 on page 350 Ramsey.

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 a.out ml.sml.

Hints, guidelines, and test code

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

Extra Credit

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

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

• README, telling us with whom you collaborated, how long you worked, what parts you finished (including any extra credit), and so on.
  
• stest.sml, containing your answer to Exercise S
• ttest.nml, containing your answer to Exercise T
• ml.sml, containing a completely interpreter for nano-ML which includes your answers to Exercises 15, 16, and 17.

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

How your work will be evaluated

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