CSE341: Programming Languages Lecture 25 Subtyping for Records and Functions Dan Grossman Fall 2011Last major course topic: more types • SML and Java have static type systems to prevent some errors – ML: No such thing as a "treated number as function" error – Java: No such thing as a "message missing" error – Etc. • What should the type of an object be? – Theory: • What fields it has (and what types of things they hold) • What methods it has (and argument/result types) – With Ruby style getters/setters, no need to treat fields separately – Common practice: • Use the names of classes and interfaces instead – Has plusses and minuses; see next lecture Fall 2011 2 CSE341: Programming LanguagesBeing more flexible • ML's type system would be much more painful (reject safe programs you want to write) without parametric polymorphism – Also known as generics – Example: A separate length function for int list and string list • Java's type system would be much more painful (reject safe programs you want to write) without subtype polymorphism – Also known as subtyping – Example: Couldn't pass an instance of a subtype when expecting an instance of a supertype – (Yes, Java also has generics as a separate concept) Fall 2011 3 CSE341: Programming LanguagesSo which is better? • Generics and subtyping are best for different things – And you can combine them in interesting ways – But that's for next lecture because… • First we need to learn how subtyping works! – Classes, interfaces, objects, methods, etc. will get in the way at first (we'll get there) – So start with just subtyping for records with mutable fields – We will make up our own syntax • ML has records, but no subtyping or field-mutation • Racket and Ruby have no type system • Java uses class/interface names and rarely fits on a slide Fall 2011 4 CSE341: Programming LanguagesRecords (half like ML, half like Java) Record expression (field names and contents): Evaluate ei, make a record Record field access: Evaluate e to record v with an f field, get contents Record field update Evaluate e1 to a record v1 and e2 to a value v2; Change v1's f field (which must exist) to v2; Return v2 Fall 2011 5 CSE341: Programming Languages {f1=e1, f2=e2, …, fn=en} e.f e1.f = e2A Basic Type System Record types: What fields a record has and type of contents Type-checking expressions: • If e1 has type t1, …, en has type tn, then {f1=e1, …, fn=en} has type {f1:t1, …, fn:tn} • If e has a record type containing f : t, then e.f has type t • If e1 has a record type containing f : t and e2 has type t, then e1.f = e2 has type t Fall 2011 6 CSE341: Programming Languages {f1:t1, f2:t2, …, fn:tn}This is safe These evaluation rules and typing rules prevent ever trying to access a field of a record that does not exist Example program that type-checks (in a made-up language): Fall 2011 7 CSE341: Programming Languages fun distToOrigin (p:{x:real,y:real}) = Math.sqrt(p.x*p.x + p.y*p.y) val pythag : {x:real,y:real} = {x=3.0, y=4.0} val five : real = distToOrigin(pythag)Motivating subtyping But according to our typing rules, this program does not type-check – It does nothing wrong and seems worth supporting Fall 2011 8 CSE341: Programming Languages fun distToOrigin (p:{x:real,y:real}) = Math.sqrt(p.x*p.x + p.y*p.y) val c : {x:real,y:real,color:string} = {x=3.0, y=4.0, color="green"} val five : real = distToOrigin(c)A good idea: allow extra fields Natural idea: If an expression has type {f1:t1, f2:t2, …, fn:tn} Then it can also have a type missing some of the fields This is what we need to type-check these function calls: Fall 2011 9 CSE341: Programming Languages fun distToOrigin (p:{x:real,y:real}) = … fun makePurple (p:{color:string}) = … val c :{x:real,y:real,color:string} = {x=3.0, y=4.0, color="green"} val _ = distToOrigin(c) val _ = makePurple(c)Keeping subtyping separate A programming language already has a lot of typing rules and we don't want to change them – Example: The type of an actual function argument must equal the type of the function parameter We can do this by adding "just two things to our language" – Subtyping: Write t1 <: t2 for t1 is a subtype of t2 – One new typing rule that uses subtyping: If e has type t1 and t1 <: t2, then e (also) has type t2 So now we just have to define t1 <: t2 Fall 2011 10 CSE341: Programming LanguagesSubtyping is not a matter of opinion • Misconception: If we are making a new language, we can have whatever typing and subtyping rules we want • Well, not if you want to prevent what you claim to prevent – Here: No accessing record fields that don't exist • Our typing rules were sound before we added subtyping – So we better keep it that way • Principle of substitutability: If t1 <: t2, then any value of type t1 must be able to be used in every way a t2 can be – Here: It needs all the same fields Fall 2011 11 CSE341: Programming LanguagesFour good rules For our record types, these rules all meet the substitutability test: 1. "Width" subtyping: A supertype can have a subset of fields with the same types 2. "Permutation" subtyping: A supertype can have the same set of fields with the same types in a different order 3. Transitivity: If t1 <: t2 and t2 <: t3, then t1 <: t3 4. Reflexivity: Every type is a subtype of itself (4) may seem unnecessary, but it composes well with other rules in a full language and "can't hurt" Fall 2011 12 CSE341: Programming LanguagesBut this still is not allowed [Warning: I'm tricking you into doing a bad thing ] Subtyping rules so far let us drop fields but not change their types Example: A circle has a center field holding another record For this to type-check, we need: {center:{x:real,y:real,z:real}, r:real} <: {center:{x:real,y:real}, r:real} Fall 2011 13 CSE341: Programming Languages fun circleY (c:{center:{x:real,y:real}, r:real}) = c.center.y val sphere:{center:{x:real,y:real,z:real}, r:real}) ={center={x=3.0,y=4.0,z=0.0}, r=1.0} val _ = circleY(sphere)Don't have this subtyping – could we? {center:{x:real,y:real,z:real}, r:real} <: {center:{x:real,y:real}, r:real} • No way to get this yet: we can drop center, drop r, or permute order, but we can't "reach into a field type" to do subtyping • So why not add another subtyping rule… "Depth" subtyping: If
View Full Document
Unlocking...