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

Getting the code

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

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

Two exercises to do by yourself (10%)

Six 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 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 exercises, here are some additional remarks and suggestions.

• Understand the most difficult part of a constraint solver.
  Complete Exercise 13 on page 336 of Ramsey.

• Implement a constraint solver
  Complete Exercise 16 on page 337 of Ramsey. Take advantage of the debugging redefinition of standardize shown below. 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, try to show your solver code to the course staff.

• Plan for type inference
  Complete Exercise 4 on page 334 of Ramsey. Put your answer in file rules.pdf.

• Implement type inference
  Complete Exercise 17 on page 337 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

The algorithm for standardizing a constraint calls for a lot of case analysis. I found it easier to implement this case analysis by splitting standardize into two functions:

• Function standardize handles all three forms of constraint: trivial constraints, simple type-equality constraints and conjunctions. When it sees a conjunction, it does a case analysis on the left conjunct.

• Function standardize does not do anything with simple type equalities. When standardize sees a simple type equality, either at top level or as the left child of /\, it calls the following function:

    val standardizeEqAnd : ty * ty * con -> (name * ty) list
  

  A call to standardizeEqAnd(tau_1, tau_2, C) returns a standard form of the constraint tau_1 =*= tau_2 /\ C. This function implements all the rules in Figure 7.1 that relate to simple type-equality constraints.

To help you with the solver, once you have implemented standardize, the following code redefines standardize into a version that checks itself for sanity. It guarantees that the standard form you produce implies the constraint you were given. This is not quite as good as checking for equivalence, but it is a lot better than no checking at all.

  val standardize = fn c => 
    let val std = standardize c
        val theta = standardSubstitution std
    in  if solves (theta, c) then
          std
        else
          let fun eqAnd ((a, t'), c) = TYVAR a =*= t' /\ c
              val msgs =
                    [ "Constraint ", constraintString (untriviate c), "\n  reduces to"
                    , constraintString (untriviate (foldr eqAnd TRIVIAL std))
                    , "\n  but substitution yields "
                    , constraintString (untriviate (consubst theta c)), "\n"
                    ]
          in  raise BugInTypeInference (concat msgs)
          end

    end

  val _ = if isInStandardForm std then ()
          else raise BugInTypeInference "not in standard form"

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. The splitting is covered in detail in the book, on pages 310–312. This math is subtle here, and you may find this part of the book heavy going. The last lecture on type inference will be on how to implement this splitting.

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

• As you write standardize, it's a common mistake to overlook the lessons of Exercise 13. Check the types that are inferred for the functions in the initial basis—if they are too general, the fault is probably here.

• Another 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 µ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.
  Your README file should also contain your answer to Exercise 13.
• stest.sml, containing your answer to Exercise S
• ttest.uml, containing your answer to Exercise T
• rules.pdf, containing your answer to Exercise 4
• ml.sml, containing a completely interpreter for µML which includes your answers to Exercises 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.