ML 4 Unification Algorithm Solution

Change Log




1.0 Initial Release.




 
Objectives




Your objective for this assignment is to understand the details of the basic algorithm for first order unification.




 
Preliminaries




In MP3 you implemented the first part of the type inferencer for the PicoML language. In this ML you will im-plement the second step of the inferencer: the unification algorithm unify that solves constraints generated by the inferencer. The unifier in MP3 was a black box that gave you the solution when fed the constraints generated by your implementation of the inferencer.




It is recommended that before or in tandem with completing this assignment, you go over lecture notes covering type inference and unification as well as the solution to MP3 to have a good understanding of how types are inferred.




 
Datatypes for Type Inference




Below is some of the code available for your use in the Common module. This module includes the following data types to represent the types of PicoML, which you should recognize from MP3:




type typeVar = int




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




You can use string of monoTy in common to convert your types into a readable concrete syntax for types.







 
Substitutions




In MP3, one of the things we returned was a substitution. Our substitutions have the type (typeVar * monoTy) list. The first component of a pair is the index (or “name”) of a type variable. The second is the type that should be substituted for that type variable.




In this ML, you will implement a function subst fun that will take a substitution and return a substitution function, a function that takes a type variable as input and returns the replacement type as given by the substitution. (Recall that we are using the the type int for type variables, which we give the synonym typeVar.) When creating such a function from a substitution (i.e., a list of pairs as described above), if a given type variable does not have an










1



entry in the list, the identity substitution is assumed for that type variable (i.e. the variable is substituted with itself). For instance, the substitution




 
let phi = [(5, mk_fun_ty bool_ty (TyVar(2)))];; val phi : (int * monoTy) list =

[(5, TyConst ("-", [TyConst ("bool", []); TyVar 2]))]




is considered to represent the subsitution function

( i) =
i
!


2
otherwise


bool




if i = 5



Throughout this ML you may assume that substitutions we work on are always well-structured: there are no two pairs in a substitution list with the same index.




As described above, your function subst fun should, given a substitution, return the function it represents. This should be a function that takes a typeVar and returns a monoTy.







# let subst_fun s = ...

val subst_fun : (typeVar * monoTy) list - typeVar - monoTy = <fun

# let subst = subst_fun phi;;




val subst : typeVar - monoTy = <fun




# subst 1;;




 
: monoTy = TyVar 1




# subst 5;;




 
: monoTy = TyConst ("-", [TyConst ("bool", []); TyVar 2])




We can also lift a substitution to operate on types. A substitution , when lifted, replaces all the type vari-ables occurring in its input type with the corresponding types. In this ML you will be implementing a function monoTy lift subst for lifting substitutions to generic monoTys.







# let rec monoTy_lift_subst s = ...

val monoTy_lift_subst : (typeVar * monoTy) list - monoTy - monoTy = <fun




 
let lifted_sub = monoTy_lift_subst phi;; val lifted_sub : monoTy - monoTy = <fun




 
lifted_sub (TyConst ("-", [TyVar 1; TyVar 5]));; - : monoTy =




TyConst ("-", [TyVar 1; TyConst ("-", [TyConst ("bool", []); TyVar 2])])




 
Unification




The unification algorithm takes a set of pairs of types that are supposed to be equal. A system of constraints looks like the following set




f(s1; t1); (s2; t2); :::; (sn; tn)g




Each pair is called an equation. A (lifted) substitution solves an equation (s; t) if (s) = (t). It solves a constraint set if (si) = (ti) for every (si; ti) in the constraint set. The unification algorithm will return a substitution that solves the given constraint set (if a solution exists).




You will remember from lecture that the unification algorithm consists of four transformations. These transforma-tions can be expressed in terms of how an action on the first element of the unification problem affects the remaining elements.




Given a constraint set C




 
If C is empty, return the identity substitution.




 
If C is not empty, pick an equation (s; t) 2 C. Let C0 be C n f(s; t)g.




2



 
Delete rule: If s and t are are equal, discard the pair, and unify C0 .




 
Orient rule: If t is a variable, and s is not, then discard (s; t), and unify f(t; s)g [ C0 .




 
Decompose rule: If s = TyConst(name; [s1; : : : ; sn]) and t = TyConst(name; [t1; : : : ; tn]), then discard (s; t), and unify C0 [ Sni=1f(si; ti)g.

 
Eliminate rule: If s is a variable, and s does not occur in t, substitute s with t in C0 to get C00 . Let be the substitution resulting from unifying C00 . Return updated with s 7! (t).




 
If none of the above cases apply, it is a unification error (your unify function should return the None option in this case).




In our system, function, integer, list, etc. types are the terms; TyVars are the variables.



 
Problems




 
(0 pts) Make sure that you understand the monoTy data type. You should be comfortable with how to represent a type using monoTy. MP3 should have given you enough practice of this. If you still do not feel fluent enough, do the exercise below. This exercise will not be graded; it is intended to warm you up.




In each item below, define a function asMonoTyX:unit - monoTy that returns the monoTy representation of the given type. In these types, ; ; ; ; ::: are type variables.




bool ! int list




 
let asMonoTy1 () = ...




val asMonoTy1 : unit - monoTy = <fun




 
string_of_monoTy(asMonoTy1());; - : string = "bool - int list"




! ! !




 
let asMonoTy2 () = ...




val asMonoTy2 : unit - monoTy = <fun




 
string_of_monoTy(asMonoTy2());;




- : string = "’d - ’c - ’b - ’a"




! ( int)list




 
let asMonoTy3 () = ...




val asMonoTy3 : unit - monoTy = <fun




# string_of_monoTy(asMonoTy3());;

 
: string = "’f - (’e * int) list"




(string ( list ! ))




# let asMonoTy4 () = ...




val asMonoTy4 : unit - monoTy = <fun




# string_of_monoTy(asMonoTy4());;

 
: string = "string * ’h list - ’g"







 
(4 pts) Implement the subst fun function as described in Section 5.




 
let subst_fun s = ...




val subst_fun : (typeVar * monoTy) list - typeVar - monoTy = <fun




 
let subst = subst_fun [(5, mk_fun_ty bool_ty (TyVar(2)))];; val subst : typeVar - monoTy = <fun




 
subst 1;;




 
: monoTy = TyVar 1




# subst 5;;




 
: monoTy = TyConst ("-", [TyConst ("bool", []); TyVar 2])







 
(4 pts) Implement the monoTy lift subst function as described in Section 5.




# let rec monoTy_lift_subst s = ...

val monoTy_lift_subst : (typeVar * monoTy) list - monoTy - monoTy = <fun

# monoTy_lift_subst [(5, mk_fun_ty bool_ty (TyVar(2)))]




(TyConst ("-", [TyVar 1; TyVar 5]));;




- : monoTy =




TyConst ("-", [TyVar 1; TyConst ("-", [TyConst ("bool", []); TyVar 2])])


 
(5 pts) Write a function occurs : typeVar - monoTy - bool. The first argument is the integer com-ponent of a TyVar. The second is a target expression. The output indicates whether the variable occurs within the target.




# let rec occurs v ty = ...




val occurs : typeVar - monoTy - bool = <fun




 
occurs 0 (TyConst ("-", [TyVar 0; TyVar 0]));; - : bool = true




 
occurs 0 (TyConst ("-", [TyVar 1; TyVar 2]));; - : bool = false













 
(64 pts) Now you are ready to write the unification function. We will represent constraint sets simply by lists. If there exists a solution to a set of constraints (i.e., a substitution that solves the set), your function should return Some of that substitution. Otherwise it should return None. Here’s a sample run.




 
let rec unify eqlst = ...

val unify : (monoTy * monoTy) list - substitution option = <fun




 
let Some(subst) = unify [(TyVar 0,




TyConst ("list", [TyConst ("int", [])]));




(TyConst ("-", [TyVar 0; TyVar 0]),




TyConst ("-", [TyVar 0; TyVar 1]))];;

... (* Warning message suppressed *)

val subst : substitution =




[(0, TyConst ("list", [TyConst ("int", [])])); (1, TyConst ("list", [TyConst ("int", [])]))]




# subst_fun subst 0;;




 
: monoTy = TyConst ("list", [TyConst ("int", [])])




# subst_fun subst 1;;




 
: monoTy = TyConst ("list", [TyConst ("int", [])])




# subst_fun subst 2;;




 
: monoTy = TyVar 2




Hint: You will find the functions you implemented in Problems 2,3,4 very useful in some rules.




Point distribution: Delete is 6 pts, Orient is 6 pts, Decompose is 16 pts, Eliminate is 36 pts. This distribution is approximate. Correctness of one part impacts the functioning of other parts. We will handle this problem in the testing center in a manner similar to what we did in ML3.







 
Extra Credit (10 pts) Two types 1 and 2 are equivalent if there exist two substitutions 1; 2 such that 1( 1) = 2 and 2( 2) = 1. Write a function equiv_types : monoTy - monoTy - bool to indicate whether the two input type expressions are equivalent.




Hint: find 3 such that 1 is equivalent to 3 and 2 is also equivalent to 3 by reducing 1 and 2 to a canonical form.




# let equiv_types ty1 ty2 = ...




val equiv_types : monoTy - monoTy - bool = <fun





# equiv_types




(TyConst ("-", [TyVar 4; TyConst ("-", [TyVar 3; TyVar 4])])) (TyConst ("-", [TyVar 3; TyConst ("-", [TyVar 4; TyVar 3])]));;




 
: bool = true




# equiv_types




(TyConst ("-", [TyVar 4; TyConst ("-", [TyVar 3; TyVar 4])])) (TyConst ("-", [TyVar 4; TyConst ("-", [TyVar 3; TyVar 2])]));;




 
: bool = false