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

git clone linux.cs.tufts.edu:/comp/105/build-prove-compareThe code you need is in

In your answer to question 1,

Question 2 in the text is worded in a somewhat confusing way. To clarify: the typing rules of nML permit the declaration

The answers to both exercises should go into file

For the coding exercises you'll be modifying the interpreter in

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

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

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

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" endThe type-inference code will be easier to write with the aid of a summary of the nano-ML type system which I have placed online. 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

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.

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

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`

If there are errors or warnings in this step, your work will earn
No Credit for functional correctness.
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. • • Indentation is consistent everywhere. • The submission has no bracket faults. • The submission has a few minor bracket 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) • • |
• 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 • The submission contains more than a handful of parenthesized |

Names | • Type variables have names beginning with |
• Types, type variables, constraints, and substitutions mostly respect conventions, but there are some names like |
• Some names misuse standard conventions; for example, in some places, a type variable might have a name beginning with |

Structure | • The nine cases of simple type equality are handled by these five patterns: • The code for solving • 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 |
• The nine cases are handled by nine patterns: one for each pair of value constructors for • The code for • 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 |
• The case analysis for a simple type equality does not have either of the two structures on the left. • The code for • 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 |