Lecture #22: Type Inference, ContinuedSolving Simple Type EquationsMost General SolutionsFinding Most-General Solution by UnificationUnification AlgorithmExample of UnificationExpressing Type Rules of a Small LanguageUsing the Type RulesAside: CurryingExampleLecture #22: Type Inference, Continued• The issue from last time: given two type expressions defining setsof possible types, do they intersect?• A type expression is apattern. For this lecture, a type expressioncan be– Aprimitive type(int, bool);– Atype variable(today we’ll use ML notation: ’a, ’b, ‘c1, etc.);– Thetype constructorT list, where T is a type expression;– Afunction typeD → C, where D and C are type express i ons.• Will formulate our problems as systems oftype equationsbetweenpairs of type expressions.• Need to find the substitutionLast modified: Sun Mar 27 23:46:22 2005 CS164: Lecture #22 1Solving Simple Type Equations• Simple example: solve’a list = int list• Easy: ’a = int.• How about this:’a list = ’b list list; ’b li st = int list• Also easy: ’a = int list; ’b = int.• On the other hand:’a list = ’b → ’bis unsolvable: lists are not functions.• Also, if we requirefinitesolutions, then’a = ’b list; ’b = ’a listis unsolvable.Last modified: Sun Mar 27 23:46:22 2005 CS164: Lecture #22 2Most 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 → intetc.• But prefer amost generalsolution that will be compatible withanypossible solution.• Any substitution for ’a must be some kind of li st, and ’b must bethe type of element in ’a, but otherwise, no constraints• Leads to solution’a = ’b listwhere ’b remains a free type variable.• In general, our solutions look like a bun ch of equations ’ ai= Ti,where the Tiare type expression s and none of the ’aiappear in anyof the T ’s.Last modified: Sun Mar 27 23:46:22 2005 CS164: Lecture #22 3Finding Most-General Solution by Unification• Tounifytwo type exp ressions is to find substitutions for all typevariables that make the expressions identical.• The set of substitutions is called aunifier.• Represent substitutions by giving each typ e variable, ’τ , abindingto some type expression.• Initially, each variable isunbound.Last modified: Sun Mar 27 23:46:2 2 2005 CS164: Lecture #22 4Unification Algorithm• For any type expression, definebinding(T ) =binding(T0), if T is a type variable bound to T0T, 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 trueif T2 is a type variable and does not appear in T1:bind T2 to T1; return trueif 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(D 1 , D 2) and unif y ( C 1,C2)else: return falseLast modified: Sun Mar 27 23:46:2 2 2005 CS164: Lecture #22 5Example 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 a ny order), keeping thebindings from one unification to the next.’a: bool’b: ’abool’c: ’a → ’bbool → boolUnify ’b l ist, ’a lis t:Unify ’b, ’aUnify ’a→ ’b, ’cUnify ’c → bool, (bool → bool) → boolUnify ’c, bool → bool:Unify ’a → ’b, bool → bool:Unify ’a, boolUnify ’b, bool:Unify bool, boolUnify boo l, boolLast modified: Sun Mar 27 23:46:2 2 2005 CS164: Lecture #22 6Expressing Type Rules of a Small Language• In rules, read E : τ as “Expres sion E must have type τ.”• Each of the ’a, ’aimentioned is a “fresh” type variable, introducedfor each application of the rule.Construct Type ConditionsInteger literalint[] ’a l isthd (L) ’a L: ’a listtl (L) ’a list L: ’a listE1+E2int E1: int, E2: intE1::E2’a list E1: ’a, E2: ’a listE1= E2bool E1: ’a, E2: ’aE1!=E2bool E1: ’a, E2: ’aif E1then E2else E3’a E1: bool, E2: ’a, E3: ’aE1E2’b E1: ’a → ’b, E2: ’adef f x1 ...xn = E x1: ’a1, . . . , xn: ’an, E:’a0,f: ’a1→ . . . → ’an→ ’a0.Last modified: Sun Mar 27 23:46:2 2 2005 CS164: Lecture #22 7Using the Type Rules• Apply these rules to a program to get a bunch of Conditions.• Whenever two Conditions as cribe a type to the same expression,equate those types.• Solve the resulting equations.Last modified: Sun Mar 27 23:46:2 2 2005 CS164: Lecture #22 8Aside: Currying• Writingdef sqr x = x*x;means essentially that sqr is defined to have the value λ x. x*x.• To get more than one argument, writedef f x y = x + y;and f will have the value λ x. λ y. x+y• It’s type will be int → int → int (Note: → is ri g ht associative).• So, f 2 3 = (f 2) 3 = (λ y. 2 + y) (3) = 5• Zounds! It’s the CS61A substitution model!• This tri ck of turning multi-argument functions into one-argumentfunctions is ca l l edcurrying(after Haskell Curry).Last modified: Sun Mar 27 23:46:2 2 2005 CS164: Lecture #22 9Exampledef f x L = if L = [] then [] el seif x != hd(L) then f x (tl L)else x :: f x (tl L) fifi• Let’s initially us e ’f, ’ x, ’L, etc. as the fresh type variable s.• Using th e rul es then generates equati ons like this :’f = ’a0 → ’a1 → ’a2 # de f rule’L = ’a3 list # = rule, [] rule’L = ’a4 list # hd rule ,’x = ’a4 # != rule’x = ’a0 # ca ll rule’L = ’a5 list # tl rule’a1 = ’a5 list # tl rule , call rule...Last modified: Sun Mar 27 23:46:2 2 2005 CS164: Lecture #22
View Full Document
Unlocking...