Implementing uML: Hindley-Milner Type Inference [OPTIONAL]

Due Friday, May 9 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:

Complete Exercise T below, and from Chapter 7 in Ramsey, complete Exercises 15 and 16.

Getting the code

To get the code, 
  git clone linux.cs.tufts.edu:/comp/105/book-code
The code you need is in bare/uml/ml.sml.

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 µML. 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))
Naturally, you will supply your own test cases.

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

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.

Testing

The course interpreter is located in /homes/cs456/bin/uml. 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 are some common mistakes:

There are also some common assumptions which are mistaken:

What to submit

Submit these files: Use the command: 
turnin -c cs456 -p ml-inf README ttest.uml ml.sml

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
If there are errors or warnings in this step, your work will earn No Credit for functional correctness.

How your work will be evaluated

Your typing rules will be evaluated using the usual criteria for inference rules, which I won't repeat here.

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

Exemplary Satisfactory Must improve
Form

• The code has no offside violations.

• Or, the code has just a couple of minor offside violations.

• Indentation is consistent everywhere.

• The submission has no bracket faults.

• The submission has a few minor bracket faults.

• Or, the submission has no bracketed names, but a few bracketed conditions or other faults.

• The code has several offside violations, but course staff can follow what's going on without difficulty.

• In one or two places, code is not indented in the same way as structurally similar code elsewhere.

• The submission has some redundant parentheses around function applications that are under infix operators (not checked by the bracketing tool)

• Or, the submission contains a handful of bracketing faults.

• Or, the submission contains more than a handful of bracketing faults, but just a few bracketed names or conditions.

• Offside violations make it hard for course staff to follow the code.

• The code is not indented consistently.

• The submission contains more than a handful of parenthesized names as in (x)

• The submission contains more than a handful of parenthesized if conditions.
Names

• Type variables have names beginning with a; types have names beginning with t or tau; constraints have names beginning with c; substitutions have names beginning with theta; lists of things have names that begin conventionally and end in s.

• Types, type variables, constraints, and substitutions mostly respect conventions, but there are some names like x or l that aren't part of the typical convention.

• Some names misuse standard conventions; for example, in some places, a type variable might have a name beginning with t, leading a careless reader to confuse it with a type.
Structure

• The nine cases of simple type equality are handled by these five patterns: TYVAR/any, any/TYVAR, CONAPP/CONAPP, TYCON/TYCON, other.

• The code for solving α ≐ τ has exactly three cases.

• The constraint solver is implemented using an appropriate set of helper functions, each of which has a good name and a clear contract.

• Type inference for list literals has no redundant case analysis.

• Type inference for expressions has no redundant case analysis.

• In the code for type inference, course staff see how each part of the code is necessary to implement the algorithm correctly.

• Wherever possible appropriate, submission uses map, filter, foldr, and exists, either from List or from ListPair

• The nine cases are handled by nine patterns: one for each pair of value constructors for ty.

• The code for α ≐ τ has more than three cases, but the nontrivial cases all look different.

• The constraint solver is implemented using too many helper functions, but each one has a good name and a clear contract.

• The constraint solver is implemented using too few helper functions, and the course staff has some trouble understanding the solver.

• Type inference for list literals has one redundant case analysis.

• Type inference for expressions has one redundant case analysis.

• In some parts of the code for type inference, course staff see some code that they believe is more complex than is required by the typing rules.

• Submission sometimes uses a fold where map, filter, or exists could be used.

• The case analysis for a simple type equality does not have either of the two structures on the left.

• The code for α ≐ τ has more than three cases, and different nontrivial cases share duplicate or near-duplicate code.

• Course staff cannot identify the role of helper functions; course staff can't identify contracts and can't infer contracts from names.

• Type inference for list literals has more than one redundant case analysis.

• Type inference for expressions has more than one redundant case analysis.

• Course staff believe that the code is significantly more complex than what is required to implement the typing rules.

• Submission includes one or more recursive functions that could have been written without recursion by using map, filter, List.exists, or a ListPair function.