lecture 18

Slide1: 

David Evans http://www.cs.virginia.edu/~evans CS655: Programming Languages University of Virginia Computer Science Lecture 18: Deconstructing Type Reconstruction A Bill of Rights is what the people are entitled to against every government, and what no just government should refuse, or rest on inference. Thomas Jefferson (supporter of explicit types)

Menu: 

Menu Today’s Manifest – Web Only http://www.cs.virginia.edu/~cs655/manifests/apr6.html Type Inference (Reconstruction) Why polymorphism? Why implicit types? Type Judgments review How it works

Issues: 

Issues Type Polymorphism Can write a function that works for many types Try defining id in Java, C or Pascal Type Reconstruction = Type Inference Determine types statically, without explicit declarations Without polymorphism, type inference would be (nearly) trivial.

Type Inference w/o Polymorphism: 

Type Inference w/o Polymorphism All primitives have defined type. The type of a function can be determined by looking at any callsite, and tracing back the types of the actual parameters Because there is no polymorphism, the choice or callsite, and order doesn’t matter

Example: 

Example def id  fun (xid) xid   xid. xid def f  fun (xf) id (xf) f (3); f (3)  xf: typeof(3) = int id (xf )  xid: typeof(xf) = int id  fun (xid ) xid : typeof (xid )  typeof (xid ) = int  int f  fun (xf) id (xf) : typeof (xf )  typeof (id (xf)) = int  int

Example, cont.: 

Example, cont. def id  fun (xid) xid def f  fun (xf) id (xf) f ('test'); f  fun (xf) id (xf) : typeof (xf )  typeof (id (xf)) = string  string  int  int Monomorphic types: Can’t have f(3) and f('test') in the same program Polymorphic types: Simple type inference strategy doesn’t work – gives f too restrictive a type.

Polymorphism with Explicit Types: 

Polymorphism with Explicit Types No problem – just use type qualifiers. def id: .   fun (xid) xid Often, qualifiers are implicit. def id:   fun (xid) xid def length:  list  int  fun (l) if null(l) then 0 else 1 + length (tl (l)) Type checking is easy – just bind type parameters at callsite and do unification. x: float list length (x) x must match  list, so  is float

Implicit Types (Cynical Interpretation): 

Implicit Types (Cynical Interpretation) Some misguided souls think its easier to write programs without needing to declare explicit types Other less-misguided souls want a good source of research problems, ways to apply their hard-earned knowledge of formal semantics (Some people are less cynical.)

Implicit Types(Less Cynical Version): 

Implicit Types (Less Cynical Version) Explicit types clutter programs, programmers should be thinking about algorithms not types Type inference gives you the best of both worlds: Still get the static checking type safety guarantees (no run-time type errors) But, don’t have to declare explicit types

Type Inference: 

Type Inference Type Polymorphism with Implicit Types is hard FL (Aiken/Murphy) – use operational semantics Common Approach Milner 1978 (Often called 'Hindley-Milner' type reconstruction) Used in ML (originally), Haskell, etc.

Type Schema: 

Type Schema To handle polymorphism, we need unbound types ML uses `andlt;identandgt; for a generic type `a  `a `a list  int `a list  `a (`a  `b)  `a list  `b list Cardelli paper uses , , ...

Unification: 

Unification Find a substitution for type variables that is consistent, or fail if no consistent substitution exists. Types t1 and t2 are unified by a substitution s if st1= st2. unify (`a  `b, int  int) = { `a = int, `b = int } unify (int  bool, `a  int) = fail unify ((`a  `b)  `a list  `b list, `c  int list) = { `b = int, `c = (`a  int)  `a list }

Defining unify: 

Defining unify unify: type schema, type schema, substitution  substitution b1, b2: base types (types with no ` variables) unify (b1, b2, S) = if b1 = b2 then S else fail unify (`a, x, S) = if ((`a, y)  S and x  y) then fail else S  {(`a, x)} unify (`a  x, y  z, S) = S1 = unify (`a, y, S), S2 = unify (x, z, S) if S1 = fail or S2 = fail then fail else if any inconsistent matches then fail else S2 S1  S1 S2 A match (, )  S1 is inconsistent if (, )  S2 and   .

Example: 

Example unify ((`a  `b)  `a list  `b list, `c  int list, {}) S1 = unify ((`a  `b)  `a list, `c, {}) = { (`c = (`a  `b)  `a list) } S2 = unify (`b list, int list, {}) rule for list: unify (`a list, x list, S) = unify (`a, x, S) = unify (`b, int, {}) = { (`b, int) } S2 S1 = { (`c = (`a  int)  `a list) } S1 S2 = { (`b, int) } S2 S1  S1 S2 = { (`c = (`a  int)  `a list), (`b, int) }

Generating Type Schemas: 

Generating Type Schemas We need to produce type schemas for a program, and then unify those type schemas Unify works on pairs of schemas. Could define a unify that works on sets, or just unify the power set of all pairs of schemas. Primitives have defined type schemas. 0, 1, ... : int cons: (`a x `a list)  `a list

Cardelli’s Applicative Language: 

Cardelli’s Applicative Language Exp ::= Ide | if Exp then Exp else Exp | fun (Ide) Exp | Exp ( Exp ) | let Decl in Exp | ( Exp ) Decl ::= Ide = Exp | some extras we don’t care about We want a function, TCGen (Exp) that produces a set of type schemas.

TCGen(Exp): 

TCGen(Exp) TCGen (Ide) = { } TCGen (if Exp1 then Exp2 else Exp3) = { (typeof (Exp1), bool), (typeof (Exp2) , typeof (Exp3)) }  TCGen (Exp1)  TCGen (Exp2 )  TCGen (Exp3) TCGen (fun (Ide) Exp) = { (`a, typeof (Ide)) }  TCGen (Exp) where `a is free in TCGen (Exp).

TCGen(Exp), cont.: 

TCGen(Exp), cont. TCGen (Exp1 (Exp2)) = { (typeof (Exp1), `a  `b), (typeof (Exp2), `a) }  TCGen (Exp1)  TCGen (Exp2) TCGen (let Decl in Exp) = TCGenD (Decl)  TCGen (Exp) TCGenD (Ide = Exp) = { (typeof (Ide), typeof (Exp)) }  TCGen (Exp)

What is typeof?: 

What is typeof? Just something to solve constraints for: `a = typeof (E) Primitives: TCGen (Program) = TCGen (Exp)  { (typeof (0), int), (typeof (1), int), ..., (typeof (true), bool), ..., (typeof (head), `a list  `a) }

Problem: 

Problem Can use head on different types of lists in the same expression: (head (cons (fun (x) x) nil)) (head (cons (2 nil)) Shouldn’t need to unify {(typeof (head), `a list  `a), (typeof (cons (fun (x) x) nil), `a), (typeof (cons (2 nil), `a)}

Solution: 

Solution Where is the implicit ? Each instance of a function application should produce a new type constraint with new type variables: { (typeof (head1), `a list  `a), (typeof (cons (fun (x) x) nil), `a), (typeof (head2), `b list  `b), (typeof (cons (2 nil), `b)}

Type Inference: 

Type Inference Solve a system of type equations (What we just did) Prove theorems in a formal system Type judgment rules More like regular type checking, plus type variables that can be specialized using unify Elevator speech: Group 6

Typing Rules: 

Typing Rules A.x:  x:  means a type environment where x is associated with  A p: bool A ec:  A ea:       A (if p then ec else ea):  [cond] [ide]

Abstraction and Application: 

Abstraction and Application   A (fun (x) e):    [abstraction] A.x:  e:    A e(p):  [application] A e:    A p:  

Generalize and Specialize: 

Generalize and Specialize   A e: .  [generalize] A e:  for  not free in A   A e:  [/] [specialize] A e: . Substitute for type variable in .

Example: 

Example Type of (fun (x) x) 3:  x:  x:  [ide] (fun (x) x):     [abstraction] (fun (x) x): .     [generalize] [specialize] (fun (x) x): int  int   A 3: int [application] (fun (x) x) 3: int  A

Limitations: 

Limitations Self-Application (fun (x) x(x)) Good explanation why is worth .5 challenge point Handling subtype polymorphism Breaks unification algorithm Known solutions, but gets compilcated Polymorphic Function Parameters (fun (f) (pair (f 1) (f true)))

Polymorphic Parameters: 

Polymorphic Parameters What is the type of fapp = (fun (f) (pair (f 1) (f true)))? fapp (fun (x) x) has type int x bool Try (.   )  int x bool But  is inside function scope, our type schemas only allow quantifiers outside. Try . ((  )  int) But if  is outside, binds too early! ((int  int)  int) fapp (x. x + 1) is not well-typed.

Solutions?: 

Solutions? Allow quantifiers inside type schemas Requires more powerful inference rules Makes type system undecidable! Require explicit declarations ML’s solution Gives up (supposed) benefits of implicit types

Summary: 

Summary Type polymorphism enhances code reuse: can use same function for many types Type inference makes it possible to infer types statically for most (but not all) programs Problems and loss of redundant information make it highly questionable

Charge: 

Charge See http://www.plover.com/~mjd/perl/yak/typing/typing.html if you are interested in a less technical explanation of type inference and some compelling examples where it does spectacular things Next week: Parallel Programming Read Finkel chapter PS3 Due Tuesday – start it now if you haven’t already