Starting from:
$29.99
Homework 4 Monty
Please submit each answer in a separate file. The answer to the first two questions should be in a file called a4q12.sml and the answers to the other two questions should be similarly labelled, that is a4q3.txt (or .pdf) and a4q4.txt(.pdf).
In the first two questions we will implement 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 SML datatype called tp to encode these types.
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.
We can check whether two types are unifiable, using the following general scheme for transforming a set of equations between types. A set of equations is unifiable, if it can be transformed into the empty set. Otherwise, it is not unifiable: this means you get a non-empty set of equations and none of the rules below can be used to simplify the equations further.
Var α = α,C =⇒ C Int int = int ,C =⇒ C Bool bool = bool ,C =⇒ C List t list = s list ,C =⇒ t = s,C Function (t1 → t2) = (s1 → s2),C =⇒ t1 = s1,t2 = s2,C Product (t1 ∗t2) = (s1 ∗s2),C =⇒ t1 = s1,t2 = s2,C Inst 1 α = t,C =⇒ [t/α]C provided α 6∈ FV(t) Inst 2 t = α,C =⇒ [t/α]C provided α 6∈ FV(t)
Now we need to explain how we will encode all this in SML. First we have to define the
1
possible types of Monty with an inductive definition. Here is an inductive definition of the types of Monty encoded as an SML datatype.
datatype tp = Int | Bool | List of tp | Arrow of tp * tp | Cross of tp * tp | TVar of (tp option) ref
The interesting part about this data-type definition is that we represent type variables using references and option types. An uninstantiated type variable will be a reference which contains NONE. If a type variable is instantiated with some type t then it will contain SOME(t). We will destructively propagate the instantiation for a given type variable as we start solving the equations.
Question 1[25 points] Crucial to the unification algorithm is the side condition α 6∈ FV(t) in the rules Inst 1 and Inst 2. This condition is called occurs check, because we must check whether the variable α occurs in the type t. In this question you are asked to implement the following function for the occurs check.
occursCheck: (tp option) ref * tp - unit
Given a type variable a and a type t, it will return unit if a does not occur in the type t. Otherwise it will raise the exception OccursCheck.
Question 2[35 points]
In this question you are asked to implement a function unifiable which checks whether two types are unifiable.
unifiable: tp * tp - unit
The function expects two types t and s and will return unit if the two types are unifiable. As a side-effect it will instantiate destructively all the free type variables occurring in t and s. If two types t and s are not unifiable, it will raise an exception Error. Use the exception Error to propagate error messages.
Question 3[20 points] Informally derive the type for the apply-list function defined below. This function takes a list of functions and produces a single function which is the composite of all of them. If the list is empty one gets the identity function.
The code is shown below.
fun apply_list [] = (fn x = x) | apply_list(f::fs) = (fn x = apply_list(fs)(f(x)))
Question 4[20 points] Informally derive the type of the function foo below. fun foo x = x:= (!x)+1.
In the first two questions we will implement 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 SML datatype called tp to encode these types.
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.
We can check whether two types are unifiable, using the following general scheme for transforming a set of equations between types. A set of equations is unifiable, if it can be transformed into the empty set. Otherwise, it is not unifiable: this means you get a non-empty set of equations and none of the rules below can be used to simplify the equations further.
Var α = α,C =⇒ C Int int = int ,C =⇒ C Bool bool = bool ,C =⇒ C List t list = s list ,C =⇒ t = s,C Function (t1 → t2) = (s1 → s2),C =⇒ t1 = s1,t2 = s2,C Product (t1 ∗t2) = (s1 ∗s2),C =⇒ t1 = s1,t2 = s2,C Inst 1 α = t,C =⇒ [t/α]C provided α 6∈ FV(t) Inst 2 t = α,C =⇒ [t/α]C provided α 6∈ FV(t)
Now we need to explain how we will encode all this in SML. First we have to define the
1
possible types of Monty with an inductive definition. Here is an inductive definition of the types of Monty encoded as an SML datatype.
datatype tp = Int | Bool | List of tp | Arrow of tp * tp | Cross of tp * tp | TVar of (tp option) ref
The interesting part about this data-type definition is that we represent type variables using references and option types. An uninstantiated type variable will be a reference which contains NONE. If a type variable is instantiated with some type t then it will contain SOME(t). We will destructively propagate the instantiation for a given type variable as we start solving the equations.
Question 1[25 points] Crucial to the unification algorithm is the side condition α 6∈ FV(t) in the rules Inst 1 and Inst 2. This condition is called occurs check, because we must check whether the variable α occurs in the type t. In this question you are asked to implement the following function for the occurs check.
occursCheck: (tp option) ref * tp - unit
Given a type variable a and a type t, it will return unit if a does not occur in the type t. Otherwise it will raise the exception OccursCheck.
Question 2[35 points]
In this question you are asked to implement a function unifiable which checks whether two types are unifiable.
unifiable: tp * tp - unit
The function expects two types t and s and will return unit if the two types are unifiable. As a side-effect it will instantiate destructively all the free type variables occurring in t and s. If two types t and s are not unifiable, it will raise an exception Error. Use the exception Error to propagate error messages.
Question 3[20 points] Informally derive the type for the apply-list function defined below. This function takes a list of functions and produces a single function which is the composite of all of them. If the list is empty one gets the identity function.
The code is shown below.
fun apply_list [] = (fn x = x) | apply_list(f::fs) = (fn x = apply_list(fs)(f(x)))
Question 4[20 points] Informally derive the type of the function foo below. fun foo x = x:= (!x)+1.
1 file (101.4KB)
