Type InferenceCriticisms of Typed LanguagesSlide 3Type SchemesExampleStep 1: Add Type SchemesStep 2: Generate ConstraintsSlide 8Slide 9Slide 10Slide 11Slide 12Slide 13Slide 14Slide 15Slide 16Slide 17Step 3: Solve ConstraintsStep 4: Generate typesType Inference DetailsConstraint GenerationSlide 22Slide 23Slide 24Slide 25OperatorsSlide 27Slide 28Slide 29Slide 30Slide 31Slide 32Slide 33Slide 34Slide 35Slide 36If statementsSlide 38Slide 39Function ApplicationSlide 41Function DeclarationSlide 43Solving ConstraintsSubstitutionsUnificationUnification MachineSlide 48Slide 49Slide 50Slide 51Slide 52Slide 53Slide 54Occurs CheckSlide 56Unification Machine Gets StuckTerminationSlide 59Slide 60Properties of SolutionsSummary: Type InferenceCompare with Subtyping AlgorithmType InferenceDavid WalkerCOS 320Criticisms of Typed LanguagesTypes overly constrain functions & datapolymorphism makes typed constructs useful in more contextsuniversal polymorphism => code reusemodules & abstract types => code reusesubtyping => code reuseTypes clutter programs and slow down programmer productivitytype inferenceuninformative annotations may be omittedType InferenceType Inferenceoverviewgeneration of type constraints from unannotated simply-typed programsFun has subtyping and still needed some annotationsThere is an algorithm for complete type inference for MinML without subtyping (and of course for full ML, including parametric polymorphism)solving type constraintsType SchemesA type scheme contains type variables (a, b, c) that may be filled in during type inferences ::= a | int | bool | s1 -> s2A term scheme is a term that contains type schemes rather than proper typese ::= ... | fun f (x:s1) : s2 = eExamplefun map (f, l) = if null (l) then nil else cons (f (hd l), map (f, tl l)))Step 1: Add Type Schemesfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l), map (f, tl l)))type schemeson functionsStep 2: Generate Constraintsfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l), map (f, tl l)))for eachexpression,perform type inference onsub expressions,assigning themtype schemesand generatingconstraintsthat mustbe solvedStep 2: Generate Constraintsfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l), map (f, tl l)))begin with theif expression &recursivelyperform type inference on itssubexpressionsStep 2: Generate Constraintsfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l), map (f, tl l)))b = b’ list since argument to null must be a listStep 2: Generate Constraintsfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l), map (f, tl l))): d list since nil is some kind of listconstraintsb = b’ listStep 2: Generate Constraintsfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l), map (f, tl l))): d listconstraintsb = b’ listb = b’’ listb = b’’’ listsince hd and tl are functions that take list argumentsStep 2: Generate Constraintsfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l : b’’), map (f, tl l : b’’’ list))): d listconstraintsb = b’ listb = b’’ listb = b’’’ listb = b’’’ lista = aStep 2: Generate Constraintsfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l : b’’) : a’, map (f, tl l) : c)): d listconstraintsb = b’ listb = b’’ listb = b’’’ lista = ab = b’’’ lista = b’’ -> a’Step 2: Generate Constraintsfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l : b’’) : a’, map (f, tl l) : c)) : c’ list: d listconstraintsb = b’ listb = b’’ listb = b’’’ lista = ab = b’’’ lista = b’’ -> a’c = c’ lista’ = c’Step 2: Generate Constraintsfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l : b’’) : a’, map (f, tl l) : c)) : c’ list: d listconstraintsb = b’ listb = b’’ listb = b’’’ lista = ab = b’’’ lista = b’’ -> a’c = c’ lista’ = c’d list = c’ listStep 2: Generate Constraintsfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l : b’’) : a’, map (f, tl l) : c)) : c’ list: d list: d listconstraintsb = b’ listb = b’’ listb = b’’’ lista = ab = b’’’ lista = b’’ -> a’c = c’ lista’ = c’d list = c’ listd list = cStep 2: Generate Constraintsfun map (f : a, l : b) : c = if null (l) then nil else cons (f (hd l), map (f, tl l)))finalconstraintsb = b’ listb = b’’ listb = b’’’ lista = ab = b’’’ lista = b’’ -> a’c = c’ lista’ = c’d list = c’ listd list = cStep 3: Solve Constraintsfinalconstraintsb = b’ listb = b’’ listb = b’’’ lista = a...Constraint solution provides all possible solutions to type scheme annotations on termssolutiona = b’ -> c’b = b’ listc = c’ listmap (f : a -> b x : a list): b list = ...Step 4: Generate typesGenerate types from type schemesOption 1: pick an instance of the most general type when we have completed type inference on the entire programmap : (int -> int) -> int list -> int listOption 2: generate polymorphic types for program parts and continue (polymorphic) type inferencemap : ForAll (a,b,c) (a -> b) -> a list -> b listType Inference DetailsType constraints q are sets of equations between type schemesq ::= {s11 = s12, ..., sn1 = sn2} eg: {b = b’ list, a = b -> c}Constraint GenerationSyntax-directed constraint generationour algorithm crawls over abstract syntax of untyped expressions and generatesa term schemea set of constraintsAlgorithm defined as set of inference rules programming notation: tc(G, u) = (e, t, q)math notation: G |-- u => e : t, qinputsoutputsConstraint GenerationG |-- x ==> x :G |-- 3 ==> 3 :G |-- true ==> true :G |-- false ==> false :Constraint GenerationG |-- x ==> x : s, { } (if G(x) = s)G |-- 3 ==> 3 :G |-- true ==> true :G |-- false ==> false :Constraint GenerationG |-- x ==> x : s, { } (if G(x) = s)G |-- 3 ==> 3 : int, { }G |-- true ==> true :G |-- false ==> false :Constraint GenerationG |-- x ==> x : s, { } (if G(x) = s)G |-- 3 ==> 3 : int, { }G |-- true ==> true : bool, { }G |-- false ==> false : bool, {
View Full Document