Programming Languages and Paradigms Assignment 7

Assignment 7
Programming Languages and Paradigms

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