New User Special Price Expires in

Let's log you in.

Sign in with Facebook


Don't have a StudySoup account? Create one here!


Create a StudySoup account

Be part of our community, it's free to join!

Sign up with Facebook


Create your account
By creating an account you agree to StudySoup's terms and conditions and privacy policy

Already have a StudySoup account? Login here


by: Cleora Stiedemann


Marketplace > Rice University > ComputerScienence > COMP 311 > PROGRAMMING LANGUAGES
Cleora Stiedemann
Rice University
GPA 3.72

Robert Cartwright

Almost Ready


These notes were just uploaded, and will be ready to view shortly.

Purchase these notes here, or revisit this page.

Either way, we'll remind you when they're ready :)

Preview These Notes for FREE

Get a free preview of these Notes, just enter your email below.

Unlock Preview
Unlock Preview

Preview these materials now for free

Why put in your email? Get access to more of this material and other relevant free materials for your school

View Preview

About this Document

Robert Cartwright
Class Notes
25 ?




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.

Similar to COMP 311 at Rice University

Popular in ComputerScienence




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


Buy Material

Are you sure you want to buy this material for

25 Karma

Buy Material

BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.


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'

Why people love StudySoup

Jim McGreen Ohio University

"Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

Jennifer McGill UCSF Med School

"Selling my MCAT study guides and notes has been a great source of side revenue while I'm in school. Some months I'm making over $500! Plus, it makes me happy knowing that I'm helping future med students with their MCAT."

Steve Martinelli UC Los Angeles

"There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."


"Their 'Elite Notetakers' are making over $1,200/month in sales by creating high quality content that helps their classmates in a time of need."

Become an Elite Notetaker and start selling your notes online!

Refund Policy


All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email


StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here:

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.