Overview

Many programmers want the flexibility of an untyped scripting language and the reliability of a statically typed language, combined. This combination is provided by type inference. You are most likely to encounter it in Webby languages like Hack, TypeScript, and Elm, but it is also heavily used in systemsy languages like Haskell and OCaml, as well as researchy languages like Agda, Idris, and Coq/Gallina. All these languages, and many more to come, are based on the Hindley-Milner type system, which you will implement in this homework.

The homework exercises (but not reading-comprehension questions) may be done with a partner.

Setup

Clone the book code:

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

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

Dire warnings

val (left, right) = ... expression that evaluates to a pair ...

  sml-lint ml.sml

Reading comprehension

Before starting the programming problems, answer the reading-comprehension questions for this module, which you will find online. It is also OK to alternate between reading-comprehension questions and related homework questions.

Exercises, which you may do with a partner

Either on your own or with a partner, please work Exercises 8, 18, 19, and 21 from pages 457 to 460 of Build, Prove, and Compare, and the two exercises C and T below.

val eqsubst : subst * subst -> bool   (* arguments are equivalent *)
val hasSolution     : con -> bool
val hasNoSolution   : con -> bool
val hasGoodSolution : con -> bool
val solutionEquivalentTo : con * subst -> bool
       (* solution to constraint is equivalent to subst *)

val () = Unit.checkAssert "int ~ bool cannot be solved"
         (fn () => hasNoSolution (inttype ~ booltype))

val () = Unit.checkAssert "bool ~ bool can be solved"
         (fn () => hasSolution (booltype ~ booltype))

val () = Unit.checkAssert "bool ~ bool is solved by the identity substitution"
         (fn () => solutionEquivalentTo (booltype ~ booltype, idsubst))

val () = Unit.checkAssert "bool ~ 'a is solved by 'a |--> bool"
         (fn () => solutionEquivalentTo (booltype ~ TYVAR "'a", 
                                         "'a" |--> booltype))

TYVAR "a" ~ TYVAR "b" /\ TYVAR "b" ~ TYCON "bool"
CONAPP (TYCON "list", [TYVAR "a"]) ~ TYCON "int"

val constraints = 
  [ TYVAR "a" ~ TYVAR "b" /\ TYVAR "b" ~ TYCON "bool"
  , CONAPP (TYCON "list", [TYVAR "a"]) ~ TYCON "int"
  , TYCON "bool" ~ TYCON "int"
  ]

105-check-constraints constraints.sml

  nml -q < type-tests.nml

(check-type-error (lambda (x y z) (cons x y z)))
(check-type-error (+ 1 #t))
(check-type-error (lambda (x) (cons x x)))

(fst (pair x y)) == x
(snd (pair x y)) == y

Extra Credit

For extra credit, you may complete any of the following:

• Exercise 1 on page 456. Put your answers in your README file.

• Mutation, as in exercise 23(a) and (b). For additional credit you can add (c).

  For 23(b), please put the code in your README file.

• Better error messages, as in exercise 24(a), (b), and possibly (c)

• Explicit types, as in exercise 25

Except as noted above, just add your answers to your file ml.sml.

If you work with a partner on the main problems but you complete extra credit by yourself, please let us know in your README file.

Of these exercises, the most interesting are probably Mutation (easy) and Explicit types (not easy).

What and how to submit

Submit these files:

• A README file containing
  • The names of the people with whom you collaborated
  • The numbers of any extra credit problems you solved
• A file rules.pdf containing your constraint-based typing rules for Begin and Lambda
• File ml.sml, implementing a complete interpreter for nano-ML which includes your answers to Exercises 18, 19, and 21.
• File regression.nml containing regression tests for your type inference
• File constraints.sml, containing your answer to Exercise C
• File type-tests.nml, containing your answer to Exercise T

As soon as you have the files listed above, run submit105-ml-inf-pair to submit a preliminary version of your work. Keep submitting until your work is complete; we grade only the last submission.

Hints and guidelines

Testing

If you call your interpreter ml.sml, you can build a standalone version in a.out by running

mosmlc -I /comp/105/lib ml.sml

Don’t overlook the “c” at the end of mosmlc. Now you can run your interpreter with ./a.out, and you can run tests by

./a.out -q < /dev/null              # runs internal Unit tests
./a.out -q < regression.nml         # runs required regression tests
./a.out -q < type-tests.nml         # runs three selected tests (required)

A common mistake is to run your regression tests against my working nml interpreter. To help you test your own code, we provide a script called test-my-nml. If you’re running on the server and have run use comp105, then just run the command

test-my-nml

The script searches the current working directory for your compiled nano-ML interpreter, which must be called a.out. Then it runs a.out on your regression.nml file. (If the interpreter or the regression tests are missing, the script complains.) Or you can supply another test file:

test-my-nml moretests.nml

The nine-step design process

Working on larger codes, it’s easy to lose track of the design process. Here’s what we recommend:

• For the type checker, use the specialized techniques described in design lesson 5 (program design with typing rules).

• For the constraint solver, the standard nine-step process applies. In particular,

  • As presented in lecture, there are 9 forms of simple type-equality constraint (formed with the ~ value constructor). For most forms, you will want two examples: one that is solvable and one that is not. (Some forms have only unsolvable examples.) You will want a unit test for each.

  • There are also two other forms of constraint: conjunction constraints and the trivial constraint. You will want many examples of conjunction constraints, but to develop these examples, you will rely less on forms of data and more about ideas on substitution that you will explore in recitation.

The constraint solver

A simple type-equality constraint has nine possible cases. We recommend unit testing each one. Not all cases are solvable, but for each case that may be solvable, we recommend two tests: one on a solvable constraint and one on an unsolvable constraint.

We also recommend unit testing the conjunction case. Start with examples from the book.

Once you have passed unit tests, we recommend an additional consistency check: The following code redefines solve into a version that checks itself for idempotence. To make sure that every solution generated during type inference is in fact idempotent, use this code before typeof.

fun isIdempotent 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 isIdempotent theta then theta
                else raise BugInTypeInference "non-idempotent substitution"
            end

Type inference

With your solver in place, type inference should be mostly straightforward.

Follow the same step-by-step procedure you used to build your type checker for Typed μScheme. In particular,

• Start by disabling the predefined functions.
• Build on the partially complete implementation of typeof from the book.
• Build your implementation of literal just as you did for Typed μScheme: numbers, symbols, and Booleans first.
• Create a file of regression tests. Start with literals.
• Look at each case in the code that raises LeftAsExercise. Fix these cases one at a time. At each step, add to your regression suite, and run all the tests. Whenever possible, include check-type-error tests.
• The two difficult cases are 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 the book in the section on “Generalization in Milner’s let binding”, which is part of section 7.5.2. Look especially at the sidebar “Generalization with constraints” on page 436.
• Implement list literals toward the end.

• Before you submit your code, re-enable the predefined functions and make sure your interpreter infers the proper types for the predefined functions of nano-ML:

  (check-principal-type map     (forall ['a 'b] (('a -> 'b) (list 'a) -> (list 'b))))
  (check-principal-type filter  (forall ['a]    (('a -> bool) (list 'a) -> (list 'a))))
  (check-principal-type exists? (forall ['a]    (('a -> bool) (list 'a) -> bool)))
  (check-principal-type foldr   (forall ['a 'b] (('a 'b -> 'b) 'b (list 'a) -> 'b)))

It pays to create a lot of regression tests, of both the check-principal-type and the check-type-error variety. (The check-type test also has its place, but for this assignment, you want to stick to check-principal-type.) The most effective tests of your algorithm will use check-type-error. Assigning types to well-typed terms is good, but most mistakes are made in code that should reject an ill-typed term, but doesn’t. Here are some examples of the sorts of tests that are really useful:

(check-type-error (lambda (x) (cons x x)))
(check-type-error (lambda (x) (cdr (pair x x)))) ; only after you implement pair

Once your interpreter is rejecting ill-typed terms, if it can process the predefined functions and infer their principal types correctly, you are doing well. As a larger integration test, we have posted a functional topological sort. It contains some type tests as well as a check-expect.

Debugging

If you need to look at internal data structures, use functions eprint and eprintln to print values. These printing functions expect strings, which you can produce using these string-conversion functions:

val expString   : exp -> string
val defString   : def -> string
val typeString  : ty -> string
val constraintString : con -> string
val substString : subst -> string

All these functions are included in the interpreter’s source code.

Avoid common mistakes

How your work will be evaluated

Your constraint solving and type inference will be evaluated through extensive testing. We must be able to compile your solution in Moscow ML by typing, e.g.,

mosmlc -I /comp/105/lib ml.sml

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

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

Names

Code structure