Assignment 7 Solution

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 de ne 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 uni cation which is part of the type reconstruction algorithm for Monty. Let us recap basic facts about uni cation rst. Uni cation is one of the central operations in type-reconstruction algorithms, theorem proving and logic programming systems. In the context of type-reconstruction, uni cation tries to nd 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 uni able.




Here is the de nition 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 de nition 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 uni cation for Monty type expressions. This means nding 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 uni able 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 pre xing 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 uni able? 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 nding the most general uni er.




Question 1[40 points]




In this question you will implement some of the auxiliary functions needed for uni cation. 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 o the TypVar constructor so we need a function of the following type.




occurCheck : v:char - tau:typExp - bool




A substitution is de ned 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 uni able and produces the uni er if there is one. It should return the most general uni er or fail with an appropriate error message.




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












































































































































































3