MiniML Typechecker

Due Monday, October 21 at 2pm

In this assignment, you will build a typechecker for MiniML. Your typechecker should handle the entire syntax of MiniML. Your typechecker must also properly handle recursive functions.

There are a few issues discussed in class that you will not be responsible for handling properly.

You need not implement the value restriction. (It happens to be unnecessary in this version of the interpreter, since MiniML lacks ML-style references.)
You need not keep track of which type variables are generalizable and which are not. (You will have to deal with this distinction, however, when we get to the implementation of type inference.) Instead, your typechecker may treat all type variables as generalizable. This simplification means that your typechecker will actually be unsound! That is, it will be possible for a program to typecheck but still have a run-time type error.

You can start the assignment from the version of MiniML in /cse/courses/cse505/02au/hw2. This is the same interpreter as used in the first assignment, with the following augmentations:

hw2_solution.x86-linux is a linux binary of the sample solution for this homework -- a complete MiniML typechecker. To use it, invoke the MiniML interpreter from a linux machine as follows:
```
sml @SMLload=hw2_solution.x86-linux
```
This will start up the MiniML interpreter directly; there is no need to invoke repl(); subsequently.
hw2_solution_sound.x86-linux is a linux binary of a sound version of the sample solution. This version keeps track of which type variables are generalizable and which are not, treating them accordingly.
eval.sml contains a complete implementation of the MiniML evaluator, including proper handling of recursive functions. Feel free to use your own eval.sml from the first assignment if you'd like.
env.sml contains the Environment type and associated functionality, as before. However, it now also contains a type TypeEnvironment and associated functionality. Type environments map variables in the current scope to their types and will play an analogous role in typechecking that environments play in evaluation.
type_subst.sml defines a type TypeSubstitution, which is a mapping from type variables to types, and associated functionality. Type substitutions will be useful when typechecking the invocation of a polymorphic function. In that case, the argument type may not match the function's domain type exactly, but will instead be a particular instantiation of the domain type. A type substitution represents this instantiation by describing how type variables in the domain type are instantiated by types of the argument type. For example, if id is the identity function, of type 'a->'a, then id(3) typechecks and has type int, with 'a instantiated with int.
typecheck.sml contains the MiniML typechecker. It is currently quite incomplete; your job is to finish it. We have provided some helper functions for typechecking calls to unary and binary operators as well as calls to user-defined functions.

Unlike with the evaluator, we have not provided a template for the overall structure of the typechecker. Instead, we provide descriptions of some of the interesting aspects of the assignment:

Type annotations: Some declarations, expressions, and patterns have optional type annotations as part of their syntax (see ast.sml). In order to perform typechecking, you should require such annotations to always be provided, raising a type error otherwise.

Type equality: To test whether two Types are equal, you may use "=". This is not as precise as it could be, because we should be able to sometimes treat a function of type 'a->'a as also having the type 'b->'b. However, allowing type variables to be arbitrarily interchangeable would make this unsound interpreter even more unsound. The problem is that only generalizable type variables should be interchangeable in this way.

Top-level: Top-level declarations are typechecked by typechecking the associated declaration and returning any new bindings for the type environment. Top-level expressions are typechecked by typechecking the associated expression and returning a type environment with a binding that maps "it" to the expression's type.

Declarations: A declaration is typechecked in the context of a type environment, returning type bindings for any variables introduced by the declaration.

To typecheck a variable declaration, first typecheck its pattern, producing a type for the pattern and type bindings for variables in the pattern. Then typecheck the right-hand side, producing its type. Check that the types of the pattern and the right-hand side agree. Return the bindings produced by typechecking the pattern.
To typecheck a function declaration, typecheck each of its cases, ensuring that they agree on the function's name and type. Before typechecking each case, add the function's type to the environment, to support recursive references. The function's type can be determined by peeking at the first function case: typechecking its pattern will yield the function's argument type, and the case will have an explicitly annotated result type. (As a slight relaxation of the requirement that all optional types be present, you may allow function cases other than the first one in a function to omit the optional result type.)
To typecheck a case, typecheck its pattern to produce the case's argument type and type bindings for variables in the pattern. Then typecheck the case's body in the context of the current type environment extended with the new bindings, producing the case's result type. If the case has an explicit result type, make sure it agrees with the body's type.

Expressions: An expression is typechecked in the context of a type environment and produces the expression's type. Some representative cases follow.

To typecheck a function call, lookup the function's type in the type environment and typecheck the argument to produce its type. Ensure that the function's type is a valid function type. Then ensure that the argument type is a legal instantiation of the function's domain type (see the function check_instantiation in typecheck.sml). This check should produce a type substitution, which is then used to compute the appropriate result type as an instantiation of the function's range type (see the function apply_type_subst in type_subst.sml).
To typecheck a conditional expression, typecheck the test and make sure it has type bool. Then typecheck the two branches and make sure their types agree.
To typecheck a let, typecheck the first declaration to produce a set of new bindings. Then extend the current type environment with these new bindings and recursively typecheck the rest of the declarations. Finally, typecheck the body expression in the fully extended environment and return the type of the body.

Patterns: Typechecking a pattern returns the type of values that match the pattern and a set of type bindings for variables introduced by the pattern. It is a type error if a pattern introduces the same variable name twice. The function combine_envs_no_dups in env.sml will be useful for checking this.

How and what to turn in

Send Todd email with your typecheck.sml file as an attachment. For extra credit, also provide an example of a function that typechecks in the unsound typechecker but not in the sound typechecker, and illustrate how that function can cause a run-time type error when invoked.