## Description

In this assignment we will implement part of a type checker for a new made-up language called

Monty. In this assignment we are looking exclusively at the part of Monty that deals with its type

system. We will define an OCaml type called typExp to encode the types of Monty. Note that

Monty has a polymorphic type system.

We will use this to implement unification which is part of the type reconstruction algorithm for

Monty. Let us recap basic facts about unification first. Unification is one of the central operations

in type-reconstruction algorithms, theorem proving and logic programming systems. In the context

of type-reconstruction, unification tries to find an instantiation for the free variables in two types

τ1 and τ2 such the two types are syntactically identical. If such an instantiation exists, we say the

two types τ1 and τ2 are unifiable.

Here is the definition of the types of Monty. Remember we are writing a program in OCaml that

deals with another language (Monty). Do not confuse the types of the language Monty with OCaml

types. The type definition below is written in OCaml it describes the types of Monty.

type typExp =

| TypInt

| TypVar of char

| Arrow of typExp * typExp

| Lst of typExp

We want to implement unification for Monty type expressions. This means finding a substitution

for the type variables. A substitution is a list of pairs; each pait gives a type expression for a type

variable. We say that two type expressions are unifiable if there is a substitution that makes them

identical. This is key step in the type reconstruction algorithm.

We are using simple characters to represent type variables with the constructor TypVar prefixing

it. In the substitution we just write the character and not this constructor but this is just for

convenience. I have only got one base type (TypInt) and one unary type constructor (Lst) and one

binary type constructor (Arrow). A type that we would write as int → (‘a → ‘b − list) would be

written in our representation as

Arrow(TypInt, Arrow(TypVar ’a’, Lst (TypVar ’b’)))

The above is an example of a polymorphic type expression. Here is another one:

1

Arrow(TypVar ’a’, Arrow (TypInt, Lst (TypInt)))

These are, of course, not the same. Are they unifiable? In other words, is there some replacement

for the type variables that makes these two type expressions identical? Yes there is! If we replace

both the type variables with TypInt they will both be identical. This is the kind of thing that we

will write our program to discover. Here is a script of the program in action.

let te1 = Arrow(TypInt, Arrow(TypVar ’c’, TypVar ’a’));;

val te1 : typExp = Arrow (TypInt, Arrow (TypVar ’c’, TypVar ’a’))

# let te3 = Arrow(TypVar ’a’,Arrow (TypVar ’b’,TypVar ’c’));;

val te3 : typExp = Arrow (TypVar ’a’, Arrow (TypVar ’b’, TypVar ’c’))

# let result = unify te1 te3;;

val result : substitution = [(’b’, TypInt); (’c’, TypVar ’b’); (’a’, TypInt)]

# applySubst result te1;;

– : typExp = Arrow (TypInt, Arrow (TypInt, TypInt))

# applySubst result te3;;

– : typExp = Arrow (TypInt, Arrow (TypInt, TypInt))

Notice that this is more than simple pattern matching. Each type expression constrains the other.

We are finding the most general unifier.

Question 1[40 points]

In this question you will implement some of the auxiliary functions needed for unification. First

of all recall that we do not allow a substitution where a variable is replaced by a type expression

containing it. So we need to check if a type variable occurs in a type expression. This is called

the “occur check.” Before we call occur check we strip off the TypVar constructor so we need a

function of the following type.

occurCheck : v:char -> tau:typExp -> bool

A substitution is defined as follows.

type substitution = (char * typExp) list

Now we want a function that performs a replacement of a variable with a type expression. This

should have the following type.

val substitute : tau1:typExp -> v:char -> tau2:typExp -> typExp

This replaces all occurrences of the type variable TypVar v with the type expression tau1 in the

type expression tau2.

The above function just does one replacement. A substituion is a whole list of these so we need

another function called applySubst

val applySubst : sigma:substitution -> tau:typExp -> typExp

applySubst should apply the substitutions in a list in order from right to left.

Question 2[60 points]

2

In this question you are asked to implement a function unify which checks whether two types are

unifiable and produces the unifier if there is one. It should return the most general unifier or fail

with an appropriate error message.

val unify : tau1:typExp -> tau2:typExp -> substitution

3