MP 3 A Unification-Based Type Inferencer Solution

 
Change Log




1.0 Initial Release.




 
Caution




This assignment can appear quite complicated at first. It is essential that you understand how all the code you will write will eventually work together. Please read through all of the instructions and the given code thoroughly before you start, so you have some idea of the big picture.




 
Objectives




Your objectives are:




Become comfortable using record types and variant types, particularly as used in giving Abstract Syntax Trees. Become comfortable with the notation for semantic specifications.




Understand the type-inference algorithm.




 
Background




One of the major objectives of this course is to provide you with the skills necessary to implement a language. There are three major components to a language implementation: the parser, the internal representation, and the interpreter1. In this ML you will work on the middle piece, the internal representation.




A language implementation represents an expression in a language with an abstract syntax tree (AST), usually implemented by means of a user-defined type. Functions can be written that use this type to perform evaluations, preprocessing, and anything that can or should be done with a language. In this ML, you will write some functions that perform type inferencing using unification. This type-inferencer will appear again as a component in several future MPs/MLs. You will be given a collection of code to support your work including types for abstract syntax trees, environments and a unification procedure in Common. You will be asked to implement the unification procedure in MP4.







1A language implementation may instead/also come with a compiler. In this course, however, we will be implementing an interpreter.






















1
4.1 Type Inferencing Overview




The pattern for type inferencing is similar to the procedure used to verify an expression has a type. The catch is that you are not told the type ahead of time; you have to figure it out as you go. The procedure is as follows:




 
Infer the types of all the subexpressions. For each subexpression, you will get back a proof tree and a substi-tution. You will incrementally apply the substitution for the proof of the judgment for one subexpression to all subsequent judgments for the remaining subexpressions.




 
Create a new proof tree from the proof trees for the subexpressions.




 
Create a new substitution by composing the substitutions of the subexpressions, together with a substitution representing any additional information learned from the application of the rule in question, if there is any.




 
Return the new proof tree and the new substitution.




 
Given Code




This semester the language for which we shall build an interpreter, which we call PicoML, is mainly a simplification of OCaml. In this assignment we shall build a type inferencer for expressions in PicoML. The file common.cmo contains compiled code to support your construction of this type inferencer. Its contents are described here.




5.1 OCaml Types for PicoML AST




Expressions in PicoML are quite similar to expressions in OCaml. The Abstract Syntax Trees for PicoML expressions are given by the following OCaml type:

type
exp = (* Exceptions will be added in later MPs *)




|
VarExp of string
(*
variables *)




|
ConstExp of const
(*
constants *)




|
MonOpAppExp of mon_op * exp
(*
% e1 - % is
a builtin monadic operator *)
|
BinOpAppExp of bin_op * exp * exp
(*
e1 % e2 - %
is
a builtin binary operator *)
|
IfExp of exp * exp * exp
(*
if e1
then e2 else e3 *)
|
AppExp of exp * exp
(*
e1 e2
*)




|
FunExp of string * exp
(*
fun
x
- e1
*)


|
LetInExp of string * exp * exp
(*
let
x
= e1 in e2 *)
|
LetRecInExp of string * string * exp *
exp
(* let rec
f x = e1 in e2 *)
|
RaiseExp of exp




(* raise e
*)
|
TryWithExp of (exp * int option * exp * (int
option *
exp) list)


(* try e with i - e1 |
j
- e1
| ... | k - en *)
This type makes use of the auxiliary types:




type
const =






BoolConst of bool


(* for true and false *)
|
IntConst of int


(* 0,1,2, ... *)
|
FloatConst of float
(* 2.1, 3.0, 5.975, ... *)
|
StringConst of string
(* "a", "hi there", ... *)
|
NilConst


(*[]*)
|
UnitConst


(*()*)
type
bin_op =






IntPlusOp
(*_+_*)
|
IntMinusOp
(*_-_*)



2


|
IntTimesOp
(*
_*_*)
|
IntDivOp
(*
_/_*)
|
FloatPlusOp
(*
_+._*)
|
FloatMinusOp
(*
_-._*)
|
FloatTimesOp
(*
_*._*)
|
FloatDivOp
(*
_/._*)
|
ConcatOp
(*
_ˆ_*)
|
ConsOp
(*
_::_*)
|
CommaOp
(*
_,_*)
|
EqOp
(*
_=_*)
|
GreaterOp
(*
__*)
type
mon_op =






IntNegOp
(* integer negation *)
|
HdOp
(* hd
*)
|
TlOp
(* tl
*)
|
FstOp
(* fst *)
|
SndOp
(* snd *)
for representing the constants, binary, and unary operations in our language. Any of these types may be expanded in future MPs/MLs in order to enrich the language.




Some of the constructors of exp should be self-explanatory. Names of constants are represented by the type const. Names of variables are represented by strings. BinOpAppExp takes the binary operator, represented by the type bin op, together with two operands. Similarly, MonOpAppExp takes the unary operator of the mon op type and an operand.




The constructors that take string arguments (VarExp, FunExp, LetInExp, LetRecInExp, Let, and LetRec) use strings to represent names of variables that they bind.




We have added in RaiseExp and TryWith for raising and handling exceptions, but have limited exceptions to integers, rather in the style of Unix. We use int option in place of int to allow for a catchall pattern.




The function string of exp converts expressions into a string using a more readable form, similar to OCaml concrete syntax.







5.2 OCaml Types for PicoML Types




In addition to having abstract syntax trees for the expressions of PicoML, we need to have abstract syntax trees for the types of PicoML. The types of PicoML can be categorized into two kinds: monomorphic types and polymorphic types. Monomorphic types are simple: type variables, and type constructors applied to a sequence of types. To make these types uniform, we will consider type constants as type constructors applied to an empty sequence of types. Thus we may use the following OCaml type to represent the monomorphic types of PicoML:

type monoTy = TyVar of typeVar | TyConst of (string * monoTy list)




Type variables will just be represented by integers:




type typeVar = int




Again, there is a companion function string of monoTy that generates a string containing a more readable form of the monoTy, similar to OCaml concrete syntax for types.




Polymorphic types in PicoML are universally quantified monomorphic types. We will represent the quantified (and thus bound) type variables by a list of typeVar:

type polyTy = typeVar list * monoTy (* the list is for quantified variables *)




Again, there is a function string of polyTy that gives a more readable form of a given polyTy.




A monomorphic type can be considered as a polyTy where the list of quantified type variables is the empty list.







3



When inferring types, you will need to generate fresh type-variable names. For this, you may use the side-effecting function fresh that takes unit and returns a fresh type variable. The index stored by fresh (initially set to 0) will keep on growing as you use fresh.




5.3 Environments




We need an environment to store the types of the variables. Later, we will need environments to store values for the variables for use during execution. The idea of an environment and the operations we perform over them is independent of the information stored for each variable. An environment in general will be represented by a list of pairs mapping variables (strings) to information (types here, values later):

type ’a env = (string * ’a) list




One interacts with environments using the following functions, pre-defined in common.ml:




(*environment operations*)






let make_env x y = ...


(*create env with single pair*)
let rec lookup_env gamma x
= ... (*look
up x in gamma*)
let sum_env delta gamma = ...
(*update gamma with all mappings in delta*)
let ins_env gamma x y = ...


(*insert x-y into gamma*)
val make_env : string - ’a - ’a
env =
<fun
val lookup_env : ’a env -
string
- ’a
option = <fun
val sum_env : ’a env - ’a
env -
’a env = <fun
val ins_env : ’a env - string -
’a -
’a env = <fun






For convenience, since we will only use environments supplying polymorphic types we supply an abbreviation for that specialized type:




type type_env = polyTy env







5.4 Signatures




In addition to the environment, which will change over the course of executing programs, we need a way to store the types of constants and built-in unary and binary operators in PicoML. Unlike the environment, the signature will be fixed throughout type inference, and is provided here as three functions,







val const_signature : const - polyTy = <fun




val binop_signature : binop - polyTy = <fun




val monop_signature : monop - polyTy = <fun




taking respectively a const, a binop, or monop, and returning a polyTy.




Some constants and operators, like NilConst, ConsOp, and CommaOp have true polymorphic types, with quan-tified type variables. During type inference, it will be necessary to create distinct monomorphic instances of their polymorphic types, replacing all instances of the quantified variables with fresh variables. For instance, consider the expression







((true :: []), (0 :: []))




(We use the more familiar OCaml-like notation rather than abstract syntax that we have implemented to represent it.) When typing this expression, we shall eventually get to type both its immediate subexpressions, (true :: []) and (0 :: []), separately:













4



 
When typing (true :: []), we discover that the operator :: and constant NilConst are used with the types bool - bool list - bool list and bool list, respectively; this should be consistent with the types of :: and [] stored in our signature, namely with respectively 8 : - list - list and 8 : list (where is a type variable, written in OCaml as TyVar 0). In order for :: to be applied to true (and NilConst), we need to replace all instances of (in both types) to bool.




 
Similarly, from typing (0 :: []), we get we need to replace all instances of by int.




The two constraints, = bool and = int, are inconsistent (i.e., have no solution), since they would lead to bool = int. Thus, we have done something wrong above, because we will certainly want to allow the use of :: and NilConst polymorphically, dealing with lists of arbitrary types, in particular with lists of booleans and with lists of integers. The above problem comes from binding the same type variable, to both bool and int - this is not a proper use of the polymorphic variable , since within a fixed problem the type varaible should be instantiated everywhere with the same type. The solution is to replace with a fresh type variable each time we type the operator :: and the constant []; this way, the constraints are: 1 list = bool list and 2 - 2 list - 2 list = bool - bool list - bool list from typing (true :: []), and 3 list = int list and 4 - 4 list - 4 list = int - int list - int list from typing (0 :: []), yielding the solution 1 = 2 =bool and 3 = 4 =int.




With the signatures for constants and built-in unary and binary operators, we provide polymorphism for the built in constants and binary operators. For those constants and operators like NilConst and ConsOp, every time their type is requested from the appropriate signature, a new type with fresh type variables is given. The code for these signatures is as follows:




let bool_ty = TyConst("bool",[])




let int_ty = TyConst ("int", [])




let float_ty = TyConst ("float",[])




let string_ty = TyConst ("string",[])




let unit_ty = TyConst("unit", [])

let mk_pair_ty ty1 ty2 = TyConst("*",[ty1;ty2])

let mk_fun_ty ty1 ty2 = TyConst("-",[ty1;ty2])




let mk_list_ty ty = TyConst("list",[ty])




type polyTy = typeVar list * monoTy (* the list is for quantified variables *)




let int_op_ty = polyTy_of_monoTy(mk_fun_ty int_ty (mk_fun_ty int_ty int_ty)) let float_op_ty =




polyTy_of_monoTy(mk_fun_ty float_ty (mk_fun_ty float_ty float_ty)) let string_op_ty =




polyTy_of_monoTy(mk_fun_ty string_ty (mk_fun_ty string_ty string_ty))




(* fixed signatures *)

let const_signature const = match const with




BoolConst b - polyTy_of_monoTy bool_ty




| IntConst n - ([], int_ty)




| FloatConst f - ([], float_ty)




| StringConst s - ([], string_ty)




| NilConst - ([0],mk_list_ty (TyVar 0))




| UnitConst - ([], unit_ty)




let binop_signature binop = match binop with




IntPlusOp - int_op_ty




| IntMinusOp - int_op_ty




| IntTimesOp - int_op_ty




5



| IntDivOp - int_op_ty




| FloatPlusOp
- float_op_ty
| FloatMinusOp
- float_op_ty
|
FloatTimesOp
- float_op_ty
|
FloatDivOp
- float_op_ty



 
ConcatOp - string_op_ty




 
ConsOp -




let alpha = TyVar 0 in ([0],




mk_fun_ty alpha (mk_fun_ty (mk_list_ty alpha) (mk_list_ty alpha))) | CommaOp -




let alpha = TyVar 0 in




let beta = TyVar 1 in




([0;1],




mk_fun_ty alpha (mk_fun_ty beta (mk_pair_ty alpha beta)))




 
EqOp -




let alpha = TyVar 0 in ([0],mk_fun_ty alpha (mk_fun_ty alpha bool_ty))




 
GreaterOp -




let alpha = TyVar 0 in ([0],mk_fun_ty alpha (mk_fun_ty alpha bool_ty))




let monop_signature monop = match monop with




 
HdOp - let alpha = TyVar 0 in([0], mk_fun_ty (mk_list_ty alpha) alpha)




 
TlOp - let alpha = TyVar 0 in




([0], mk_fun_ty (mk_list_ty alpha) (mk_list_ty alpha))




 
IntNegOp - ([], mk_fun_ty int_ty int_ty)




 
FstOp -




let alpha = TyVar 0 in let beta = TyVar 1 in




([0;1], mk_fun_ty (mk_pair_ty alpha beta) alpha)




 
SndOp -




let alpha = TyVar 0 in let beta = TyVar 1 in




([0;1], mk_fun_ty (mk_pair_ty alpha beta) beta)




To be able to use different instances of these polymorphic types, as well as those occurring in our typing environ-ments, we have provided you with a function freshInstance : polyTy - monoTy that returns an instance where all the quantified variables have been replaced by fresh variables.




5.5 Type Judgments and Proofs




From the lectures, you know that an expression type judgment has the form ‘ e : . This says that in the environment , the expression e has type .




A proof is recursively defined as a (possibly empty) sequence of proofs together with the judgment being proved.




Judgments and proofs are represented by the following data types:




type judgment =

ExpJudgment of type_env * exp * monoTy




type proof = Proof of proof list * judgment




The pre-defined functions string of exp and string of proof generate more readable forms of these typing judgments and proofs. The function string of proof generates string for the proof, which when printed is in a tree-like form, with the root at the top, upside-down from the way we are used to seeing proofs.










6
5.6 Substitutions




In this ML, you are asked to write code returning, among other things, a substitution. A substitution, in its most basic form, is a partial mapping from variables to expressions. In our case, we will use substitutions from type variables to monomorphic types. In a similar manner to what we did with environments, we represent substitutions as lists:

type substitution = (typeVar * monoTy) list




Just as with environments, we need a collection of functions to operate with them. To apply a substitution to each of monomoprhic types, polymporphic types and environments, you are given the following functions:







val monoTy_lift_subst : substitution - monoTy - monoTy




val polyTy_lift_subst : substitution - polyTy - polyTy




val env_lift_subst : substitution - env - env




You also need to be able to create the substitution that represents the composition of two substitutions. If s1 and s2 are two substitutions, then







val subst_compose : substitution - substitution - substitution




can be used to generate their composition.




subst compose s1 s2 = s1 s2







That is, it creates a substitution that has the same effect as first applying the substitution s2 and then applying s1. (Warning: the order in which you apply subsitutions often matters!)




You will start generating the substitutions to be composed by applying unification to a list of constraints implied by the rule you are implementing. A constraint is represented by a pair of monomorphic types, with the intention being that you need to make them equal by filling in their variables with a substitution. The function

val unify : (monoTy * monoTy) list - substitution option







returns Some of a substitution simultaneously satisfying all the constraints in the input list, if there is one, and None if no solution exists. You will be implementing this function in MP4.




The last function you will need that we supply is one for generalizing a monomorphic type with respect to a typing environment to a polymorphic type where all the variables that do not occur (free) in the range of the environment are universally quantified in the polymorphic type created.







val gen : type_env - monoTy - polyTy




 
Type Inferencing




The rules used for a type-inferencer are derived from the rules for the type system shown in class. The additional complication is that we assume at each step that we do not fully know the types to be checked for each expression. Therefore, as we progress we must accumulate our knowledge in the form of a substitution telling us what we have learned so far about our type variables in both the type we wish to verify and the typing environment. To do so, we supplement our typing judgments with one extra component, a typing substitution. Here’s an example:




‘ e1 : int j 1 1( ‘ e2 : int j 2







‘ e1 + e2 : j unifyf( 2 1( ); int )g 2 1




The “j” is just some notation to separate the substitution from the expression. You can pronounce it as “subject to”. This rule says that the substitution sufficient to guarantee that the result of adding two expressions e1 and e2 will have type is the composition of the substitution 1 guaranteeing that e1 has type int , the substitution 2 guaranteeing that e2 has type int (when the knowledge from 1 is applied to our assumptions), and the substitution generated from the constraint the f = int g.




For example, suppose you want to infer the type of fun x - x + 2. In English, the reasoning would go like this.




7



 
Let = fg.




 
We start with a “guess” that fun x - x + 2 has type ’a.




 
Next we examine fun x - x + 2 and see that it is a fun. We don’t know what x will be, so we let it have




type ’b. Add that to and try to infer the type of the body is ’c . . .




 
Examine x + 2. We apply the above rule, so we need to infer the subtypes.




 
Examine x. says that x has type ’b. We are trying to show it has type int . We generate the substitution solving the constraint f’b = int g.

 
Examine 2. This is an integer, as needed. (To be really thorough we would add the substitution solving the constraint fint = int g.)


 
We combine these inferences together to make a new proof-tree, and add to the combined substitutions the substitution solving the constraint that says the result of applying the combination of the two substitutions known so far to ’c must be the same as int. We need to compose the substitution solving this constraint to the substitutions making ’b be type int, and int be type int. (Yes, that last one was trivial, but the rule says we have to do it. It amounts to composing wth the identity function.)




 
Now we’re ready to come back to the type of the whole expression. The variable x has type ’b, and the output has type ’c, but the whole expression has type ’a, so ’a must also be ’b - ’c. But, from above we have already learned that ’b = int and that ’c = int, and recorded this in our substitutions. Applying the substitutions accumulated so far to the constraint that ’a = ’b - ’c, we generate the substitution that solves ’a = int - int.




 
The result of our combined substitutions tell us that we need to rewrite ’b and ’c to int everywhere, and rewrite ’a to int - int everywhere. In particular, we get a final type of int - int.




6.1 Pre-defined Testing Functions




Some important functions for testing your code are pre-defined: The function infer exp takes in a function gather exp ty substitution, an env, and an exp, and returns an (monoTy * proof) option. The first part of the result type is the type of the entire expression and the second part is a proof (assuming success).




infer exp works by generating a fresh type variable and calling the function




gather exp ty substitution and gets back a (generic) proof tree and a substitution. If gather exp ty substitution returns None, then infer exp returns None. Otherwise, infer exp applies the substitution to to obtain the ultimate type. This ultimate type as well as the proof are then returned in a Some of a pair.







The functions get proof and get ty extract the proof and type parts, respectively (or raise an exception on None).







val infer_exp :

(type_env - exp - monoTy - (proof * substitution) option) - type_env - exp - (monoTy * proof) option

val get_ty : (’a * ’b) option - ’a

val get_proof : (’a * ’b) option - ’b




The verbose form of infer exp::







val niceInfer_exp :

(type_env - exp - monoTy - (proof * substitution) option) - type_env - exp - string




that prints out details about the substitution that is gathered, and the results of applying the substitution to the original fresh type. You will see these functions used in examples below.




8
 
Problems: Your task




The body of the main type inferencing function, infer exp is already implemented. Your task is to finish the implementation of the main function needed by infer exp: gather exp ty substitution : type env - exp - monoTy - (proof * substitution) option takes in a type environment, an expression, and a type and returns None (on failure), or Some of a pair of a generic proof tree containing type variables, and a substitution. The type environment is already in the proof tree, but it will be most convenient for our algorithm to hand it back directly as well, since we will always immediately need it. In each case, when the substitution returned is applied to the proof tree returned, the result is a fully valid type derivation.




To help you get started, we will give you the clause for gather exp ty substitution for a constant expres-sion:







match exp




with ConstExp c -




let tau’ = const_signature c in




(match unify [(tau, freshInstance tau’)]




with None - None




 
Some sigma - Some(Proof([],judgment), sigma)) | _ - raise (Failure "Not implemented yet")




This implements the rule







‘ c : j unifyf( ; freshInstance( 0))g




where c is a special constant, and 0 is an instance of the type assigned by the constant’s signature.

A sample execution would be:




# print_string(string_of_proof(get_proof(




infer_exp gather_exp_ty_substitution [] (ConstExp (BoolConst true)))));;




{} |= true : bool




To see what happened in greater details, we may do:




# print_string




(niceInfer_exp gather_exp_ty_substitution [] (ConstExp(BoolConst true)));;




{} |= true : ’b




Unifying substitution: [’b -- bool]




Substituting...




{} |= true : bool




It is not necessary for your work to generate exactly the same substitution that our solution gives. What is required is that the type you get for an expression must be an instance of the type the standard solution gets, and the type given by the standard solution must be an instance of the type you give. As a result, running niceInfer on the standard solution will give one way that the type inference could proceed, but it likely is not the only way.




1. (5 pts) Implement the rule for variables:




‘ x : j unifyf( ; freshInstance( x)))g where x is a program variable







Note that x) represents looking up the value of x in . In OCaml, one writes Ml3common.lookup env gamma x where x is the string naming the variable.







A sample execution is




9



# print_string (niceInfer_exp gather_exp_ty_substitution




(make_env "f" ([0], mk_fun_ty bool_ty (TyVar 0)))




(VarExp "f"));;




{f : Forall ’a. bool - ’a} |= f : ’b




Unifying substitution: [’b -- bool - ’c]




Substituting...




{f : Forall ’a. bool - ’a} |= f : bool - ’c










2. (10 pts) Implement the rule for built-in binary and unary operators:






‘ e1 : 1 j 1 1( ‘ e2 : 2 j 2
‘ e1
e2 : j unifyf( 2 1( 1 ! 2 ! ); freshInstance( 0))g 2 1


‘ e1 : 1 j




‘ e1 : j unifyf( ( 1 ! ); freshInstance( 0))g



where is a built-in binary or unary operator, and 0 is an instance of the type assigned by the signature for the built-in operator.




A sample execution would be:




# print_string (niceInfer_exp gather_exp_ty_substitution []




(BinOpAppExp(ConsOp, ConstExp (IntConst 62), ConstExp NilConst)));;




{} |= 62 :: [] : ’b




|--{} |= 62 : ’c




|--{} |= [] : ’d




Unifying substitution: [’b -- int list; ’e -- int; ’f -- int; ’d -- int list; ’c -- int]




Substituting...




{} |= 62 :: [] : int list




|--{} |= 62 : int




|--{} |= [] : int list




- : unit = ()




 
print_string (niceInfer_exp gather_exp_ty_substitution [] (MonOpAppExp(IntNegOp, ConstExp(IntConst 42))));;




{} |= ˜ 42 : ’b




|--{} |= 42 : ’c




Unifying substitution: [’b -- int; ’c -- int] Substituting...







{} |= ˜ 42 : int




|--{} |= 42 : int




- : unit = ()




10



Please note that your results on these and all other problems may look different and still be correct. For example, the order of the terms in substitutions is not fixed. Moreover, if you choose fresh variables for subterms in a different order than we did, your answer would still be correct while assigning the type variables differently.







3. (10 pts) Implement the rule for if then else:







‘ e1 : bool j 1 1( ‘ e2 : 1( ) j 2 2 1( ‘ e3 : 2 1( ) j 3







‘ if e1 then e2 else e3 : j 3 2 1




For this problem, you will have to recursively construct proofs with constraints for each of the subexpressions, and then use these results to build the final proof and constraints.




Here is a sample execution:




 
print_string (niceInfer_exp gather_exp_ty_substitution [] (IfExp(ConstExp(BoolConst true),




ConstExp(IntConst 62), ConstExp(IntConst 252))));;




{} |= if
true
then 62 else 252 : ’b
|--{} |=
true
: bool
|--{} |=
62 : ’b
|--{} |=
252 : int
Unifying substitution: [’b -- int]
Substituting...


{} |= if
true then 62 else 252 : int
|--{} |=
true : bool
|--{} |=
62 : int
|--{} |=
252 : int



- : unit = ()










 
(10pts) Implement the function rule:




[x : 1] + ‘ e : 2 j







‘ fun x - e : j unifyf( ( ); ( 1 ! 2))g




Here is a sample execution:




 
print_string (niceInfer_exp gather_exp_ty_substitution [] (FunExp("x", BinOpAppExp(IntPlusOp, VarExp "x", VarExp "x"))));;




{} |= fun x - x + x
: ’b
|--{x : ’c} |= x + x
: ’d
|--{x : ’c}
|=
x
:
’e
|--{x : ’c}
|=
x
:
’f
Unifying substitution:
[’b -- int - int; ’d -- int; ’c -- int; ’f -- int; ’e -- int]



11



Substituting...




{} |= fun x - x + x : int - int




|--{x : int} |= x + x : int




|--{x : int} |= x : int




|--{x : int} |= x : int




- : unit = ()










 
(10 pts) Implement the rule for application:




‘ e1 : 1 ! j 1 1( ‘ e2 : 1( 1) j 2







‘ e1e2 : j 2 1




Here is a sample execution:




 
print_string (niceInfer_exp gather_exp_ty_substitution [] (AppExp(FunExp("x", BinOpAppExp(IntPlusOp, VarExp "x", VarExp "x")), ConstExp(IntConst 62))));;







{} |= (fun x - x + x) 62 : ’b




|--{} |= fun x - x + x : ’c - ’b




 
|--{x : ’d} |= x + x : ’e




 
|--{x : ’d} |= x : ’f




 
|--{x : ’d} |= x : ’g |--{} |= 62 : int




Unifying substitution: [’b -- int; ’c -- int; ’e -- int; ’d -- int; ’g -- int; ’f -- int] Substituting...







{} |= (fun x - x + x) 62 : int




|--{} |= fun x - x + x : int - int




 
|--{x : int} |= x + x : int




 
|--{x : int} |= x : int




 
|--{x : int} |= x : int |--{} |= 62 : int




 
: unit = ()










 
(7 pts) Implement the rule for raise




‘ e : int j




‘ raise e : j







Here is a sample execution:




 
print_string (niceInfer_exp gather_exp_ty_substitution [] (RaiseExp(IfExp(ConstExp(BoolConst true), ConstExp(IntConst 62),




ConstExp(IntConst 252)))));;




{} |= raise if true then 62 else 252 : ’b




|--{} |= if true then 62 else 252 : int




|--{} |= true : bool




12



|--{} |= 62 : int




|--{} |= 252 : int




Unifying substitution: []




Substituting...




{} |= raise if true then 62 else 252 : ’b




|--{} |= if true then 62 else 252 : int




|--{} |= true : bool




|--{} |= 62 : int




|--{} |= 252 : int




- : unit = ()










 
(5 pts) Implement the rule for LetInExp.




‘ e1 : 1 j 1 [x : GEN( 1( ; 1( 1))] + 1( ‘ e : 1( ) j 2







‘ (let x=e1in e) : j 2 1




Here is the sample execution:




# print_string(niceInfer_exp gather_exp_ty_substitution []




(LetInExp("x", ConstExp (IntConst 7), BinOpAppExp(IntPlusOp, VarExp "x", VarExp "x"))));;




{} |= let x = 7 in x + x : ’b




|--{} |= 7 : ’c




|--{x : int} |= x + x : ’b




|--{x : int} |= x : ’d




|--{x : int} |= x : ’e




Unifying substitution: [’b -- int; ’e -- int; ’d -- int; ’c -- int] Substituting...







{} |= let x = 7 in x + x : int




|--{} |= 7 : int




|--{x : int} |= x + x : int




|--{x : int} |= x : int




|--{x : int} |= x : int




- : unit = ()










 
(5 pts) Implement the rule for LetRecInExp.




[x : 1] + [f : 1 ! 2] + ‘ e1 : 2 j 1 [f : GEN( 1( ; 1( 1 ! 2))] + 1( ‘ e : 1( ) j 2







‘ (let rec f x = e1 in e) : j 2 1




Here is the sample execution:







# print_string(niceInfer_exp gather_exp_ty_substitution []




13



(LetRecInExp("length",




"list",




IfExp(BinOpAppExp(EqOp, VarExp "list", ConstExp NilConst), ConstExp (IntConst 0),




BinOpAppExp(IntPlusOp, ConstExp (IntConst 1),




(AppExp(VarExp "length",




MonOpAppExp(TlOp,VarExp "list"))))),




AppExp(VarExp "length",




BinOpAppExp(ConsOp,




ConstExp (IntConst 2),




ConstExp NilConst)))));;




{} |= let rec length list = if list = [] then 0




else 1 + (length (tl list)) in length (2 :: []) : ’b




|--{length : ’c - ’d, list : ’c} |= if list = [] then 0




else 1 + (length (tl list)) : ’d




 
|--{length : ’c - ’d, list : ’c} |= list = [] : bool




 
| |--{length : ’c - ’d, list : ’c} |= list : ’e




 
| |--{length : ’c - ’d, list : ’c} |= [] : ’f




 
|--{length : ’g list - ’d, list : ’g list} |= 0 : ’d




 
|--{length : ’g list - int, list : ’g list} |= 1 + (length (tl list)) : int




 
|--{length : ’g list - int, list : ’g list} |= 1 : ’i




 
|--{length : ’g list - int, list : ’g list} |= length (tl list) : ’j




 
|--{length : ’g list - int, list : ’g list} |= length : ’k - ’j




 
|--{length : ’g list - int, list : ’g list} |= tl list : ’g list




 
|--{length : ’g list - int, list : ’g list} |= list : ’l |--{length : Forall ’m. ’m list - int} |= length (2 :: []) : ’b




|--{length : Forall ’m. ’m list - int} |= length : ’n - ’b




|--{length : Forall ’a. ’a list - int} |= 2 :: [] : ’o list |--{length : Forall ’a. ’a list - int} |= 2 : ’p |--{length : Forall ’a. ’a list - int} |= [] : ’q







Unifying substitution: [’o --
int; ’r
--
int; ’s --
int; ’q -- int
list;
’p --
int; ’b
--
int; ’n --
int list; ’g
-- ’m;
’l --
’m list; ’j
-- int; ’k
-- ’m list;
’i
-- int;
’d --
int; ’h
--
’m list; ’c
-- ’m list;




’f --
’m list; ’e
-- ’m list]






Substituting...












{} |= let rec length list = if list = []
then 0








else 1 +
(length (tl list)) in length
(2
:: []) : int
|--{length : ’m list - int,
list : ’m list} |= if list = [] then
0








else
1 + (length (tl
list)) : int



 
|--{length : ’m list - int, list : ’m list} |= list = [] : bool




 
| |--{length : ’m list - int, list : ’m list} |= list : ’m list




 
| |--{length : ’m list - int, list : ’m list} |= [] : ’m list




 
|--{length : ’m list - int, list : ’m list} |= 0 : int




 
|--{length : ’m list - int, list : ’m list} |= 1 + (length (tl list)) : int




 
|--{length : ’m list - int, list : ’m list} |= 1 : int




 
|--{length : ’m list - int, list : ’m list} |= length (tl list) : int




 
|--{length : ’m list - int, list : ’m list} |= length : ’m list - int




 
|--{length : ’m list - int, list : ’m list} |= tl list : ’m list




 
|--{length : ’m list - int, list : ’m list} |= list : ’m list |--{length : Forall ’a. ’a list - int} |= length (2 :: []) : int




|--{length : Forall ’a. ’a list - int} |= length : int list - int




|--{length : Forall ’a. ’a list - int} |= 2 :: [] : int list







14



|--{length : Forall ’a. ’a list - int} |= 2 : int




|--{length : Forall ’a. ’a list - int} |= [] : int list




- : unit = ()










7.1 Extra Credit




9. (7 pts) Implement the rule for handling exceptions with try...with:




‘ e : j i 1 : : : 1 ( ‘ ei : i 1 : : : 1 ( ) j i for all i = 1 : : : m







‘ try e with n1 - e1 | : : : | nm - em) : j m : : : 1




Here is a sample execution:




# print_string (niceInfer_exp gather_exp_ty_substitution [] (TryWithExp(BinOpAppExp(ConcatOp, ConstExp(StringConst "What"),




RaiseExp(ConstExp(IntConst 3))), Some 0, ConstExp(StringConst " do you mean?"), [(None, ConstExp(StringConst " the heck?")) ])));;




{} |= try ("What" ˆ (raise 3)) with 0 - " do you mean?" | _ - " the heck?" : ’b




|--{} |= "What" ˆ (raise 3) : ’b




 
|--{} |= "What" : ’c




 
|--{} |= raise 3 : ’d




 
|--{} |= 3 : int




|--{} |= " do you mean?" : string




|--{} |= " the heck?" : string




Unifying substitution: [’b -- string; ’d -- string; ’c -- string] Substituting...







{} |= try ("What" ˆ (raise 3)) with 0 - " do you mean?" | _ - " the heck?" : string




|--{} |= "What" ˆ (raise 3) : string




 
|--{} |= "What" : string




 
|--{} |= raise 3 : string




 
|--{} |= 3 : int




|--{} |= " do you mean?" : string




|--{} |= " the heck?" : string




 
: unit = ()

















































15