DOC PREVIEW
Princeton COS 320 - Type Inference

This preview shows page 1-2-3-4-29-30-31-32-33-60-61-62-63 out of 63 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 63 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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 & datapolymorphism makes typed constructs useful in more contextsuniversal polymorphism => code reusemodules & abstract types => code reusesubtyping => code reuseTypes clutter programs and slow down programmer productivitytype inferenceuninformative annotations may be omittedType InferenceType 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 constraintsType SchemesA type scheme contains type variables (a, b, c) that may be filled in during type inferences ::= a | int | bool | s1 -> s2A term scheme is a term that contains type schemes rather than proper typese ::= ... | 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 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 listType Inference DetailsType constraints q are sets of equations between type schemesq ::= {s11 = s12, ..., sn1 = sn2} eg: {b = b’ list, a = b -> c}Constraint GenerationSyntax-directed constraint generationour algorithm crawls over abstract syntax of untyped expressions and generatesa term schemea 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

Princeton COS 320 - Type Inference

Download Type Inference
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Type Inference and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Type Inference 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?