PROGRAMMING LANGUAGES COMP 311
Popular in Course
Popular in ComputerScienence
This 11 page Class Notes was uploaded by Cleora Stiedemann on Monday October 19, 2015. The Class Notes belongs to COMP 311 at Rice University taught by Robert Cartwright in Fall. Since its upload, it has received 28 views. For similar materials see /class/224952/comp-311-rice-university in ComputerScienence at Rice University.
Reviews for PROGRAMMING LANGUAGES
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 10/19/15
Type Systems II COMP 31 1 Rice University Houston Texas Fall 2003 Copyright 2000 Robert Cartwright all rights reserved Students r 1 make copies of these materials for their personal use COMP 311 Type Systems Simply Typed Acalculus Realistic core language suitable for typechecking M c x MMM Axnzxrc M lfMthenM 122 b1xx gt1 be B a set of base types including bool CE Ca set of constants including true false 0 E C has a given type x c x E Va set of variables variables in xrc xnz must be distinct Typing rules F x x11 F c xc xtrue bool xfalse bool F M01 xx 0k gt 1 F N1zo1 1 NkIOk app rule F M N1Nkr F X1201 mm M 1 abs rule F A X1201Xk20k M 01 xx 0k gt 1 Fl M1zbool Fl Mzzo Fl Mazo if rule F if M then M2 else M3 o COMP 311 Type Systems Sample Typing Proof Show Q 7 fboolabool 7 xbaol ffx 7 xhoo x hoolabool Tree1 fboolabool xbool fboolahool fbnolabool xhnol xbool fboolabool xbool fx bool Tree2 fhoolabool xbool fboolahool Tree1 fboolabool xbool ffx bool fboolabool 7 xboo ffx hoolabool Q 7 fboolabool 7 xbool ffx boolabool aboulahoul Trees xbool xhool Q 7 xboo x hoolahool Tree4 Tree2 Tree3 Q 7 fboolahool 7 xboo ffx 7 xhool x boolabool COMP 311 Type Systems Sample Type Reconstruction Is A f 0 A x1 f f x A xv x typable What is its principal type Tree1 fox1 fo fox1x1 oo1gt02 101 fo1 02 xo1 fx 02 Tree2 f 01 a 02 x 01 f 01 a 02 Tree1 02 01 Q Afo1 o1 xo1ffxo1o1o101 Tree3 X when xvxvgtv Tree4 Tree2 Tree3 U 01 fo101 x01ffx xo1xo1 o1 COMP 311 Type Systems Formalizing Polymorphism One extension to the simply typed language Ietx M in M where let is recursive scope of x includes the right hand side of definition of x Five extensions to our simple type system 7 Type variables a1 a2 7 Type schemes 0 V011 Ck 1 where 1 is atype Type schemes are not types 7 Type environments symbol tables can contain type schemes so can the table x 7 Additional inference rules I c V011 01k 1 x OPENVcc1 Ck 1 51 k instantiation 51 5k are types I c11 M11 I cCLOSE11 F M1 letpoly I I letx M in N1 7 Additional axiom I c OPENxc 51 k where CE C and 30 V011 Ck 1 COMP 311 Type Systems Formalizing Polymorphism continued Notes 7 The notation OPENVcc1 CkT 51 k means convertthe type scheme 1 Ck 1 to the type 1 where 1 is 1 with type variables 11 Ck replaced by fresh type variables 51 k 7 The notation CLOSE11I means convert the type 11 to the type scheme Vcc1 CkT1 where 011 Ck are the type variables that appear in 11 but not I Intuition Polymorphism abbreviates brute force replication of the definition introduced in a let The new type variables that appear in the type of M rhs of the let binding are arbitrary The instantiation and polylet rules lets us adapt a symbolic type for M to each of the specific uses of x the lhs of the let binding in N the body ofthe let The rhs side ofthe let binding cannot use xpolymorphically because such usage is inconsistent with the fact that polymorphic let is an abbreviation mechanism COMP 311 Type Systems Sample Polymorphic Type Reconstruction Consider afunctional language with polymorphic lists The operations on polymorphic lists include the binary function cons unary functions first and rest and the constant null A sample program in this language is let length A x if null x then 0 else 1 length rest x in length cons 1 null length cons true null Can we type it Sketch Q length cc list int Use letpoly rule to add length to type environment with polymorphic type lnstantiate it twice once for bool and once for int COMP 311 Type Systems Sample Polymorphic Type Reconstruction Claim 31 Iet1engtn M if nu11 x1then0 else 1 1engtn rest x in 1engtn cons1 nu11 1engtn construe nu11 int Tree1 1engtn 3lt311 nu11 oclistabool 1engtn 3 X 31 1x31 31 oclist 1engtn 3 xoclist1 nu11 x bool Tree2 1engtn 3 x urlist1 rest mrlistaazrlist 1engtn 3 x oclist1x urlist 0d a 1engtn 3 x urlist1 rest x oelist 1engtn urlista32 xoclist1 1engtn rest 0 32 3 oelistgt32 1engtn urlistaint xoclist1 1 1engtnrest x int 32 int Tree3 Tree1 1engtn urlista int Xotlist 1 0 int TreQ 1engtn urlistaint x urlist 1 if nu11 x then 0 else 1 1engtn rest x int 1engtn urlistaint 1 xx if nu11 X then 0 else 1 1engtn rest x1111 urlistaint Tree4 1engtn Vuurlistaint 1 cons wxmrlistaoarlist 1engtn Vuurlistaint 11 int 1engtn Vuurlistaint 1nu11ourist 06 ow int 1engtn Vuurlistaint 1 cons1 nu11 intrlist Tree5 1engtn Vuarlistain 1engtn mrlistaint Tree4 a5 int 1engtn Vuurllstain 1engtn cons1 nu11 int Tree6 1engtn Vaurlistaint 1cons aaxatarlistaabrlist 1engtn Vaurlistaint 1true bool 1engtn Vuurlistaint 1nu11oar list 1engtn Vouwlistaint 1 1engtn intlistaim 1engtn Vuurlistaint 1 construe nu11 boolrlist 1engtn Vaurlistaint 1 1engtn construe nu11 int 56 COMP 311 Type Systems Sample Polymorphic Type Reconstruction cont Tree7 Tree5 Tree6 lengthVoc alistaint int xintaint lengthVoc alistaint length consl null length construe null int Tree8 Tree3 Tree7 Q let length Ax if null x then 0 else 1 length rest x in length cons 1 null length cons true nullint COMP 311 9 Type Systems Coping with Imperativity lf replicating the let definition x M renaming the defined variable x for each use of x in M does not preserve the meaning of programs then programs written using Milner style polymorphism may not be type correct In an imperative language this phenomenon can happen in ys First the evaluation of M may have side effects Second the value of x may allocate mutable storage which is shared when x M is a single definition but split among the various type instantiations when the definition is replicate In an imperative language this splitting can be detected by mutating allocated storage To avoid this problem we can restrict Mto a form that guarantees replication does not c ange the meaning of programs This restricted form prevents Mfrom performing sideeffects and from allocating shared mutable storage If we restrict M to a syntactic value a constant variable or Aexpression then no d effect or sharing of mutable storage can occur The most modern languages that use HindleyMilner polymorphism use this restriction Standard ML uses a much more complicated and less useful restriction that is incomparable to the syntactic value test COMP 311 10 Type Systems Coping with Imperativity We can incorporate the value restriction in our type system by refining the definition of CLOSE so that it does not generalize the free type variables when then rhs of a definition is not a syntactic value Let us extend our polymorphic calculus language to imperative form in the same way that we did for Jam by adding the type constant unit the unary type constructor ref the unary operations ref a ref and refa and the binary operation 9 ref x a unit The following polymorphic imperative program generates a runtime type error even though it can be statically typed checked using our rules omitting the value restriction Ietx ref null in e xconstruenull l X 1 In the absence of the value restriction this program is typable because x has polymorphic type ref enabling each occurrence of x in the let body to be separately typed Hence the first occurrence ofx has type bool ref while the second has type int ref The value restriction prevents polymorphic generalization in this case preserving type soundness COMP 311 11
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'