Type Inference David Walker COS 320 Criticisms of Typed Languages Types overly constrain functions data polymorphism makes typed constructs useful in more contexts universal polymorphism code reuse modules abstract types code reuse subtyping code reuse Types clutter programs and slow down programmer productivity type inference uninformative annotations may be omitted Type Inference Type Inference overview generation of type constraints from unannotated simply typed programs Fun has subtyping and still needed some annotations There is an algorithm for complete type inference for MinML without subtyping and of course for full ML including parametric polymorphism solving type constraints Type Schemes A type scheme contains type variables a b c that may be filled in during type inference s a int bool s1 s2 A term scheme is a term that contains type schemes rather than proper types e fun f x s1 s2 e Example fun map f l if null l then nil else cons f hd l map f tl l Step 1 Add Type Schemes fun map f a l b c if null l then type schemes nil on functions else cons f hd l map f tl l Step 2 Generate Constraints fun map f a l b c if null l then nil else cons f hd l map f tl l for each expression perform type inference on sub expressions assigning them type schemes and generating constraints that must be solved Step 2 Generate Constraints fun map f a l b c if null l then nil else cons f hd l map f tl l begin with the if expression recursively perform type inference on its subexpressions Step 2 Generate Constraints fun map f a l b c if null l then nil b b list since argument to n must be a list else cons f hd l map f tl l Step 2 Generate Constraints constraints b b list fun map f a l b c if null l then since nil is some kind of list nil d list else cons f hd l map f tl l Step 2 Generate Constraints fun map f a l b c if null l then nil d list else cons f hd l map f tl l b b list constraints b b list b b list since hd and tl are functions that take list arguments Step 2 Generate Constraints constraints b b list b b list b b list fun map f a l b c if null l then nil d list else cons f hd l b map f tl l b list a a b b list Step 2 Generate Constraints constraints b b list b b list b b list a a b b list fun map f a l b c if null l then nil d list else cons f hd l b a map f tl l c a b a Step 2 Generate Constraints constraints b b list b b list b b list a a b b list a b a fun map f a l b c if null l then nil d list else cons f hd l b a map f tl l c c list c c list a c Step 2 Generate Constraints constraints b b list b b list b b list a a b b list a b a fun map f a l b c if null l then nil d list else cons f hd l b a map f tl l c c list d list c list c c list a c Step 2 Generate Constraints constraints b b list b b list b b list a a b b list a b a fun map f a l b c if null l then nil d list else cons f hd l b a map f tl l c c list d list d list c c c list a c d list c list Step 2 Generate Constraints fun map f a l b c if null l then nil else cons f hd l map f tl l final constraints b b list b b list b b list a a b b list a b a c c list a c d list c list d list c Step 3 Solve Constraints Constraint solution provides all possible solutions to type scheme annotations on terms final constraints b b list b b list b b list a a solution a b c b b list c c list map f a b x a list b list Step 4 Generate types Generate types from type schemes Option 1 pick an instance of the most general type when we have completed type inference on the entire program map int int int list int list Option 2 generate polymorphic types for program parts and continue polymorphic type inference map ForAll a b c a b a list b list Type Inference Details Type constraints q are sets of equations between type schemes q s11 s12 sn1 sn2 eg b b list a b c Constraint Generation Syntax directed constraint generation our algorithm crawls over abstract syntax of untyped expressions and generates a term scheme a set of constraints Algorithm defined as set of inference rules programming notation tc G u e t q math notation G u e t q inputs outputs Constraint Generation G x x G 3 3 G true true G false false Constraint Generation G x x s G 3 3 G true true G false false if G x s Constraint Generation G x x s G 3 3 int G true true G false false if G x s Constraint Generation G x x s if G x s G 3 3 int G true true bool G false false bool Operators G u1 u2 Operators G u1 G u2 G u1 u2 Operators G u1 e1 G u2 e2 G u1 u2 Operators G u1 e1 G u2 e2 G u1 u2 e1 e2 Operators G u1 e1 G u2 e2 G u1 u2 e1 e2 int Operators G u1 e1 t1 q1 G u2 e2 G u1 u2 e1 e2 int q1 U t1 int Operators G u1 e1 t1 q1 G u2 e2 t2 q2 G u1 u2 e1 e2 int q1 U q2 U t1 int t2 int Operators G u1 u2 Operators u1 e1 t1 q1 G u2 e2 t2 q2 u1 u2 e1 e2 bool Operators u1 e1 t1 q1 G u2 e2 t2 q2 u1 u2 e1 e2 bool Operators u1 e1 t1 q1 G u2 e2 t2 q2 u1 u2 e1 e2 bool q1 U q2 U t1 int t2 in If statements G if u1 then u2 else u3 If statements G u1 e1 t1 q1 G u2 e2 t2 q2 G u3 e3 t3 q3 G if u1 then u2 else u3 if e1 then e2 else e3 If statements G u1 e1 t1 q1 G u2 e2 t2 q2 G u3 e3 t3 q3 G if u1 then u2 else u3 if e1 then e2 else e3 a q1 U q2 U q3 …