Lecture 22 Type Inference Continued The issue from last time given two type expressions defining sets of possible types do they intersect A type expression is a pattern For this lecture a type expression can be A primitive type int bool A type variable today we ll use ML notation a b c1 etc The type constructor T list where T is a type expression A function type D C where D and C are type expressions Will formulate our problems as systems of type equations between pairs of type expressions Need to find the substitution Last modified Sun Mar 27 23 46 22 2005 CS164 Lecture 22 1 Solving Simple Type Equations Simple example solve a list int list Easy a int How about this a list b list list b list int list Also easy a int list b int On the other hand a list b b is unsolvable lists are not functions Also if we require finite solutions then a b list b a list is unsolvable Last modified Sun Mar 27 23 46 22 2005 CS164 Lecture 22 2 Most General Solutions Rather trickier a list b list list Clearly there are lots of solutions to this e g a int list b int a int int list b int int etc But prefer a most general solution that will be compatible with any possible solution Any substitution for a must be some kind of list and b must be the type of element in a but otherwise no constraints Leads to solution a b list where b remains a free type variable In general our solutions look like a bunch of equations ai Ti where the Ti are type expressions and none of the ai appear in any of the T s Last modified Sun Mar 27 23 46 22 2005 CS164 Lecture 22 3 Finding Most General Solution by Unification To unify two type expressions is to find substitutions for all type variables that make the expressions identical The set of substitutions is called a unifier Represent substitutions by giving each type variable a binding to some type expression Initially each variable is unbound Last modified Sun Mar 27 23 46 22 2005 CS164 Lecture 22 4 Unification Algorithm For any type expression define binding T 0 if T is a type variable bound to T 0 binding T T otherwise Now proceed recursively unify T1 T2 T1 binding T1 T2 binding T2 if T1 T2 return true if T1 is a type variable and does not appear in T2 bind T1 to T2 return true if T2 is a type variable and does not appear in T1 bind T2 to T1 return true if T1 and T2 are S1 list and S2 list return unify S1 S2 if T1 and T2 are D1 C1 and D2 C2 return unify D1 D2 and unify C1 C2 else return false Last modified Sun Mar 27 23 46 22 2005 CS164 Lecture 22 5 Example of Unification Try to solve b list a list a b c c bool bool bool bool We unify both sides of each equation in any order keeping the bindings from one unification to the next a b c Last modified Sun Mar 27 23 46 22 2005 CS164 Lecture 22 6 Example of Unification Try to solve b list a list a b c c bool bool bool bool We unify both sides of each equation in any order keeping the bindings from one unification to the next a Unify b list a list b c Last modified Sun Mar 27 23 46 22 2005 CS164 Lecture 22 6 Example of Unification Try to solve b list a list a b c c bool bool bool bool We unify both sides of each equation in any order keeping the bindings from one unification to the next a b Unify b list a Unify b a list a c Last modified Sun Mar 27 23 46 22 2005 CS164 Lecture 22 6 Example of Unification Try to solve b list a list a b c c bool bool bool bool We unify both sides of each equation in any order keeping the bindings from one unification to the next a b a c a Unify b list a Unify b a Unify a b c list b Last modified Sun Mar 27 23 46 22 2005 CS164 Lecture 22 6 Example of Unification Try to solve b list a list a b c c bool bool bool bool We unify both sides of each equation in any order keeping the bindings from one unification to the next a b c Unify b list a list Unify b a Unify a b c Unify c bool bool a a bool b Last modified Sun Mar 27 23 46 22 2005 CS164 Lecture 22 6 bool Example of Unification Try to solve b list a list a b c c bool bool bool bool We unify both sides of each equation in any order keeping the bindings from one unification to the next a b c Unify b list a list Unify b a Unify a b c Unify c bool bool Unify c bool bool a a bool b Last modified Sun Mar 27 23 46 22 2005 CS164 Lecture 22 6 bool Example of Unification Try to solve b list a list a b c c bool bool bool bool We unify both sides of each equation in any order keeping the bindings from one unification to the next a b c a a b Last modified Sun Mar 27 23 46 22 2005 Unify b list a list Unify b a Unify a b c Unify c bool bool bool Unify c bool bool Unify a b bool bool CS164 Lecture 22 6 bool Example of Unification Try to solve b list a list a b c c bool bool bool bool We unify both sides of each equation in any order keeping the bindings from one unification to the next a bool b a c a b Last modified Sun Mar 27 23 46 22 2005 Unify b list a list Unify b a Unify a b c Unify c bool bool bool Unify c bool bool Unify a b bool bool Unify a bool CS164 Lecture 22 6 bool Example of Unification Try to solve b list a list a b c c bool bool bool bool We unify both sides of each equation in any order keeping the bindings from one unification to the next a bool b a c a b Last modified Sun Mar 27 23 46 22 2005 Unify b list a list Unify b a Unify a b c Unify c bool bool bool Unify c bool bool Unify a b bool bool Unify a bool Unify b bool CS164 Lecture 22 6 bool Example of Unification Try to solve b list a list a b c c bool bool bool bool We unify both sides of each equation in any order keeping the bindings from one unification to the next a bool b a c a b Last modified Sun Mar …
View Full Document
Unlocking...