CSE341, Fall 2011, Lecture 25 SummaryStandard Disclaimer: This lecture summary is not necessarily a complete substitute for attending class,reading the associated code, etc. It is designed to be a useful resource for students who attended class andare later reviewing the material.Types for Objects (in the Next Lecture)We previously studied static types for functional programs, in particular ML’s type system. ML uses itstype system to prevent errors like treating a number as a function. A key source of expressiveness in ML’stype system (not rejecting too many programs that do nothing wrong and programmers are likely to write)is parametric polymorphism, also known as generics.So we should also study static types for object-oriented programs, such as those found in Java. If everythingis an object (which is less true in Java than in Ruby), then the main thing we would want our type systemto prevent is “method missing” errors, i.e., sending a message to an object that has no method for thatmessage. If objects have fields accessible from outside the object (e.g., in Java), then we also want to prevent“field missing” errors. There are other possible errors as well, like calling a method with the wrong numberof arguments.While languages like Java and C# have generics these days, the source of type-system expressiveness mostfundamental to object-oriented style is subtype polymorphism, also known as subtyping. ML does not havesubtyping, though this decision is really one of language design (it would complicate type inference, forexample).Our plan for this lecture and the next one is to:• Study subtyping• Compare subtyping and generics, determining which idioms are best supported by each• Combine subtyping and generics, showing that the result is even more useful than the sum of the twotechniquesSubtyping for Records and FunctionsIt would be natural to study subtyping using Java since it is a well-known object-oriented language witha type system that has subtyping. But it is also fairly complicated, using classes and interfaces for typesthat describe objects with methods, overriding, static overloading, etc. While these features have pluses andminuses, they can complicate the fundamental ideas that underlie how subtyping should work.So this lecture studies subtyping using only records (like in ML, things with named fields holding contents —basically objects with public fields, no methods, and no class names) and functions (like in ML or Racket).This will let us see how subtyping should — and should not — work, so that then the next lecture can thenapply the results to the more complicated setting of a class-based object-oriented language.This approach has the disadvantage that we cannot use any of the language we have studied: ML does nothave subtyping and record fields are immutable, Racket and Ruby are dynamically typed, and Java is toocomplicated for our starting point. So we are going to make up a language with just records, functions,variables, numbers, strings, etc. and explain the meaning of expressions and types as we go.A Made-Up Language of RecordsTo study the basic ideas behind subtyping, we will use records with mutable fields, as well as functions andother expressions. Our syntax will be a mix of ML and Java that keeps examples short and, hopefully, clear.For records, we will have expressions for making records, getting a field, and setting a field as follows:1• In the expression {f1=e1, f2=e2, ..., fn=en}, each fi is a field name and each ei is an ex-pression. The semantics is to evaluate each ei to a value vi and the result is the record value{f1=v1, f2=v2, ..., fn=vn}. So a record value is just a collection of fields, where each field has aname and a contents.• For the expression e.f, we evaluate e to a value v. If v is a record with an f field, then the result isthe contents of the f field. Our type system will ensure v has an f field.• For the expression e1.f = e2, we evaluate e1 and e2 to values v1 and v2. If v1 is a record with anf field, then we update the f field to have v2 for its contents. Our type system will ensure v1 has anf field. Like in Java, we will choose to have the result of e1.f = e2 be v2, though usually we do notuse the result of a field-update.Now we need a type system, with a form of types for records and typing rules for each of our expressions.Like in ML, let’s write record types as {f1:t1, f2:t2, ..., fn:tn}. For example, {x : real, y : real}would describe records with two fields named x and y that hold contents of type real. And{foo: {x : real, y : real}, bar : string, baz : string} would describe a record with three fieldswhere the foo field holds a (nested) record of type {x : real, y : real}. We then type-check expressionsas follows:• If e1 has type t1, e2 has type t2, ..., en has type tn, then {f1=e1, f2=e2, ..., fn=en} has type{f1:t1, f2:t2, ..., fn:tn}.• If e has a record type containing f : t, then e.f has type t (else e.f does not type-check).• If e1 has a record type containing f : t and e2 has type t, then e1.f = e2 has type t (else e1.f = e2does not type-check).Assuming the “regular” typing rules for other expressions like variables, functions, arithmetic, and functioncalls, an example like this will type-check as we would expect: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)In particular, the function distToOrigin has type {x : real, y : real} -> real, where we write func-tion types with the same syntax as in ML.This type system does what it is intended to do: No program that type-checks would, when evaluated, tryto look up a field in a record that does not have that field.Now Add SubtypingWith our typing rules so far, this program would not type-check: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)In the call distToOrigin(c), the type of the argument is {x:real,y:real,color:string} and the typethe function expects is {x:real,y:real}, breaking the typing rule that functions must be called with the2type of argument they expect. Yet the program above is safe: running it would not lead to accessing a fieldthat does not exist.A natural idea is to make our type system more lenient as follows: If some expression has a record type{f1:t1, ..., fn:tn}, then let the expression also
View Full Document
Unlocking...