I. Types and Classes in OOP (and Java) A. Basic concepts 1. type and type error ------------------------------------------ BASIC CONCEPTS OF TYPE AND CLASS def: the protocol (interface) of an object is def: a type is Some questions: - Who decides what constitutes a type? - What is a type error? ------------------------------------------ What should a type be? 2. behavioral reasoning aided by type checker can we make even stronger behavioral guarantees? ------------------------------------------ REASONING ABOUT ADTs Data type induction argument example: Sets represented by lists To prove: every Set's list has no duplicates How to prove this? ------------------------------------------ What part of the program has to be examined for this to work? 3. Seals (Morris 1973) ------------------------------------------ SEAL GOALS Only by using the ADTs ops can a client: alter = discover = Clients cannot: impersonate = SEALS MECHANISM createSeal -> (seal_t, unseal_t) gives unique seal and unseal functions Properties: unseal_t(seal_t(x)) = x unseal_t(anything else) is an error ------------------------------------------ How could these cause problems for a program that kept a table in sorted order? Does Smalltalk prevent impersonation? How does this allow for data type induction? How could we use seals to define what a "type error" means? How does this relate to security in Java? 4. static and conservative nature of type systems ------------------------------------------ TYPE SYSTEMS AS STATIC APPROXIMATIONS Does this code have a type error? int i = 0; Foo f; bool test = myReader.read_bool(); if (test) { i = i + 1; } else { f = i; } ------------------------------------------ Why are all elements of an array assumed to have the same type? ------------------------------------------ BASIC STRATEGY OF STATIC TYPE SYSTEMS Variables have a statically declared type Expresssions are assigned a type based on Examples: ------------------------------------------ 5. soundness and completeness ------------------------------------------ SOUNDNESS AND COMPLETENESS A type system is *sound* iff A type system is *complete* iff ------------------------------------------ How to prove this? B. subtyping 1. the motivation: polymorphism ------------------------------------------ POLYMORPHISM def: code is *polymorphic* if e.g., displayAll: objList objList do: [ :o | o display ] ------------------------------------------ What's the language design tradeoff here? 2. protocols, types, and behavior ------------------------------------------ PROTOCOLS, TYPES, and BEHAVIOR def: the behavioral protocol of an object is def: S is a subtype of T if def: S is a behavioral subtype of T if ------------------------------------------ What would it mean for S to not be a subtype of T? What should a behavioral subtype be? What would it mean for S to not be a behavioral subtype of T, and still be a subtype of T? 3. subtype vs. inheritance What does subtyping have to do with inheritance? What do we know about these? ------------------------------------------ SUBTYPING VS. INHERITANCE | ===================|====================== class | | subclass | | type | | subtype | | behavioral subtype | | ------------------------------------------ ------------------------------------------ ORTHOGANALITY EXAMPLE IntSetType ^ IntSetClass | subtype | IntervalType IntervalClass ------------------------------------------ How does C++ handle this? Java? What if we required subclass = subtype? What can we do to make a subclass not be a behavioral subtype? C. types in Java 1. security and types in the JVM ------------------------------------------ WHY TYPE SOUNDNESS MATTERS IN JAVA OR HOW THEORETICIAL WORK CAN MAKE YOU FAMOUS class T { SecurityManager x; ... } class U { MyObject x; ... } T t; U u; // ...somehow make u and t aliases... t.x = System.getSecurity(); MyObject m = u.x; ------------------------------------------ 2. overview (skip) ------------------------------------------ TYPES IN JAVA Types: primitive types: byte, short, int, long float, double char boolean reference types: classes, interfaces, T[] ------------------------------------------ a. primitives b. references 3. interfaces, classes and types (skip) ------------------------------------------ CLASSES AND TYPES Every class name Object is the superclass of all classes and of all array classes SUBCLASS ==> SUBTYPE class T {...} class S extends T {...} T x = new S(); CHECKED CASTING casting to a reference type generates ------------------------------------------ ------------------------------------------ INTERFACES // example public interface Colorable { byte CLEAR = 0; void setColor(byte r, byte b, byte g); } Contains declarations of: constants, and abstract methods ------------------------------------------ ------------------------------------------ INTERFACE EXTENSION public interface PointType { int x(); int y(); } public interface ColorPointType extends Colorable, PointType { byte redness(); byte greenness(); byte blueness(); } ------------------------------------------ ------------------------------------------ INTERFACE IMPLEMENTATION class ColorPoint extends Point implements ColorPointType { byte r, g, v; public ColorPoint(int xv, int yv, byte rv, byte gv, byte bv) { super(xv, yv); r = rv; g = gv; b = bv; } public byte redness() {...} public byte greenness() {...} public byte blueness() {...} ... } class PolarColorPoint implements ColorPointType { ... } ------------------------------------------ Why doesn't Java infer when a class implements a type? ------------------------------------------ EXTENSION AND IMPLEMENTATION SUMMARY Point PointType Colorable | \ / | \ / | \ / ColorPoint -------- ColorPointType / / PolarColorPoint ------------------------------------------ ------------------------------------------ USE OF INTERFACE TYPES class Demo { public static void main(String[] args){ ColorPointType myCP; if (args.length > 1) { myCP = new ColorPoint(3,4,8,9,2); } else { myCP = new PolarColorPoint(...); } ... myCP.redness() ... } } ------------------------------------------ Can Java still do type checking when interface types are used? D. inheritance and requirements on types of methods ------------------------------------------ INHERITANCE AND METHOD TYPES class Object {...} class Number extends Object {...} class Integer extends Number {...} class Point { Number x() {...} void set_x(Number xv) {...} ... } class ColorPoint extends Point { x() { ... } void set_x( xv) ... } Point myP = new ...; myP.x() myP.set_x( ------------------------------------------ What can the return type of the ColorPoint's x method be? What can the argument typ of ColorPoint's set_x method be? Why? What about exceptions? Can you allow more or less in the subclass? ------------------------------------------ STATIC OVERLOADING vs. DYNAMIC OVERRIDES (MESSAGE PASSING) class Foo { public int f (Float f) { return 1; } } class Bar extends Foo { public int f (String s) { return 2; } } // client code Foo x = new ...; x.f (new Float(3.14)); x.f ("a string"); // static type error ------------------------------------------ E. arrays and templates ------------------------------------------ ARRAYS IN JAVA Suppose ColorPoint is a subtype of Point. Is ColorPoint[] a subtype of Point[]? ------------------------------------------ ------------------------------------------ TEMPLATES What would the subtyping rule be for templates (if Java had them)? Example: Is X a subtype of X if S is a subtype of T? ------------------------------------------ How would you declare the relationships that might exist? II. Theory of OO typing A. record typing (adapted and simplified from Cardelli 88) 1. denotational semantics a. syntax ------------------------------------------ SIMPLIFIED EXPRESSIONS FOR OBJECT-ORIENTED LANGUAGES E ::= I | E_0.l(E_1) | (E_1, ..., E_n) where n >= 0 ------------------------------------------ b. domains ------------------------------------------ RECORD MODEL OF OBJECTS DOMAINS (\rho_r,\rho_c) \in REnvironment = (Identifier \FINITEARROW Data) \times (ClassId \FINITEARROW RMethDict) I \in Identifier d \in Data = Int + Bool + Object + Data* o \in Object = ClassId \times Record r \in Record = (Label \FINITEARROW Data) l,g \in Label = Identifier t \in ClassId = Identifier c \in RMethDict = (Label \FINITEARROW Method) m \in Method = Data -> (Data \union \bot) ------------------------------------------ ------------------------------------------ SEMANTIC FUNCTIONS V{|-|} \colon Expression -> REnvironment -> (Data \union \bot) V{|I|}(\rho_r,\rho_c) = \rho_r(I) V{|E_0.l(E_1)|}(\rho_r,\rho_c) = cases V{|E_0|}(\rho_r,\rho_c)} of isObject(I,r) -> \rho_c(I)(l) (inData*(inObject(I,r), V{|E_1|}(\rho_r,\rho_c))) else -> \bot end V{|(E_1,...,E_n)|}(\rho_r,\rho_c) = inData*(V{|E_1|}(\rho_r,\rho_c), ..., V{|E_n|}(\rho_r,\rho_c)) ------------------------------------------ 2. type system a. abstract syntax ------------------------------------------ ABSTRACT SYNTAX OF TYPE ATTRIBUTES RT,T,S,U \in RecordModelType D \in DataType M \in MethodType RMD \in RecordMethDictType I \in Identifier l \in Label T ::= D | M | RMD D ::= int | bool | I | (D_1, ..., D_n) where n >= 0 M ::= D_1 -> D_2 RMD ::= [l_1: M_1, ..., l_n : M_n] where n >= 0 ------------------------------------------ b. type environments ------------------------------------------ TYPE ENVIRONMENTS (\pi_r, \pi_c) \in RTypeEnv = (Identifier \FINITEARROW DataType) \times (ClassId \FINITEARROW RecordMethDictType) ------------------------------------------ How do these compare to the dynamic environment? c. meaning of type attributes ------------------------------------------ MEANING OF TYPE ATTRIBUTES TM{|-|}: RecordModelType -> (ClassId \FINITEARROW RecordMethDictType) -> Powerset(Data) TM{|int|}(\pi_c) = {inInt(i) | i \in Int} TM{|bool|}(\pi_c) = {inBool(b) | b \in Bool} TM{|I|}(\pi_c) = {inObject(I,r) | I \in dom(\pi_c), r \in RM(\pi_c(I))} TM{|(D_1,...,D_n|}(\pi_c) = {inData*(d1,...dn) | n >= 0, d1 \in TM{|D_1|}(\pi_c), ..., dn \in TM{|D_n|}(\pi_c)} RM{|[l_1:M_1, ..., l_n:M_n|}(\pi_c) = {r | dom(r) = {l_1, ..., l_n}, r(l_1) \in MM{|M_1}(\pi_c), ..., r(l_n) \in MM{|M_n}(\pi_c)} MM{|D_1 -> D_2|}(\pi_c) = { m | d1 \in TM{|D_1|}(\pi_c) ==> m(d1) \in (TM{|D_2|}(\pi_c) \union \bot)} ------------------------------------------ d. type of environments ------------------------------------------ TYPE OF ENVIRONMENTS def: (\rho_r, \rho_c) : (\pi_r, \pi_c) iff dom(\pi_r) = dom(\rho_r), dom(\pi_c) = dom(\rho_c), (\forall I \in dom(\pi_r) :: \rho_r(I) \in TM{|\pi_r(I)|}(\pi_c)), (\forall I \in dom(\pi_c) :: \rho_c(I) \in TM{|\pi_c(I)|}(\pi_c)). ------------------------------------------ What does that mean? e. subtyping rules ------------------------------------------ SUBTYPING RULES [refl] \pi_c |- T <: T \pi_c |- S <: U, \pi_c |- U <: T [tran] ---------------------------------- \pi_c |- S <: T \pi_c |- S <: T [id-1] ---------------- if (I,S) \in \pi_c \pi_c |- I <: T \pi_c |- T <: S [id-2] ---------------- if (I,S) \in \pi_c \pi_c |- T <: I \pi_c |- T' <: T, |- S <: S' [fun] ------------------------------ \pi_c |- (T -> S) <: (T' -> S') \pi_c |- T_1 <: T'_1, ..., \pi_c |- T_n <: T'_n [prod] -------------------------- if n>=0 \pi_c |- (T_1, ..., T_n) <: (T'_1, ..., T'_n) \pi_c |- T_1 <: T'_1, ..., \pi_c |- T_n <: T'_n [rmd] -------------------------- if 0<=n S], (\pi_r,\pi_c) |- E_0: T_0, (\pi_r,\pi_c) |- E_1: T_1 [msg] -------------------------------- (\pi_r,\pi_c) |- E_0.l(E_1): S (\pi_r,\pi_c) |- E_1: T_1, ..., (\pi_r,\pi_c) |- E_n: T_n [tup] -------------------------- if n>=0 (\pi_r,\pi_c) |- (E_1,...,E_n) : (T_1, ..., T_n) Lemma: If (\pi_r,\pi_c) |- E : T, then T \in DataType. ------------------------------------------ f. soundness ------------------------------------------ SOUNDNESS OF THE TYPE SYSTEM Theorem: If (\pi_r,\pi_c) |- E : T and (\rho_r,\rho_c) : (\pi_r,\pi_c), then either V{|E|}(\rho_r,\rho_c) = \bot or V{|E|}(\rho_r,\rho_c) \in TM{|T|}(\pi_c). ------------------------------------------