F-BOUNDED POLYMORPHISM PAPER Key idea: we introduce a very simple model of object-oriented programming. Objects are records (perhaps with both simple and functional types as components). No classes, no information hiding, no implementation inheritance. Examples: Here is a point object: { x=2,y=3 } Type for this object: point = {x:int, y: int} We can write: { x=2,y=3 } : point Another type: coloredpoint = {x:int, y: int, color: int} coloredpoint <= point (subset) {p1: coloredpoint, p2: point } <= {p1: point, p2: point} printable points: {x:int, y: int, print: void->string} We can view printable points as a subtype of point, and also as a subtype of printable things: {print: void->string} There is a subtype relation on record types, corresponding to the subclass relation in Simula or Smalltalk. A record type T is a subtype of another record type T' (written T <= T') if T has all of the fields of T', and possibly more, and each field of T' has a like-named field in T that is a subtype of it. Note that for any type T, T<=T, and in particular, int<=int, etc, for all of the basic types. If a has type T and T<=T', then a also has type T'. For example, (x : int, y : int, displayed : bool) <= (x : int, y : int) and so (x=3, y=4, displayed=true) : (x : int, y : int) Records can have functions as components; we can use this to model methods. The rule for subtyping among functional types is: if s' <= s and t <= t' then s->t <= s'->t' (Note that the subtype relation is inverted on the left side of the arrow. This is just another manifestation of the contravariant rule.) {maker: void->ColoredPoint} <= {maker: void->Point} {eater: Point->int} <= {eater: ColoredPoint->int} Universally quantified types: Example: a function that takes any object and returns a string for every t . t -> string Bounded quantification allows restrictions on the universally quantified variable. Example: a function that takes any printable object and returns a string. for every t \subset {print: void->string} . t -> string Problem: bounded quantification fails for recursively defined types. Ordered objects: PO = {lesseq: PO -> bool} Without F-bounded quantification, let's try to write a min function: min: for every t \subset PO . t -> t -> t Aside: this is curried. We could also write this as: min: for every t \subset PO . (t,t) -> t Now consider the Number type. Number = Rec.num { ... lesseq: num -> bool ...} Number is not a subtype of PO (because of the contravariant rule for the argument for lesseq) Instead, we need an F-bound for the variable in the type of min: F-PartialOrder[t] = { lesseq: t -> bool} (F-PartialOrder is a function from types to types) now we can give a proper type for min: min : for every t \subset F-PartialOrder[t] . t -> t -> t Pizza version of the above: WRONG WAY:: interface Ord { boolean less(Ord o) } class OrdInt implements Ord { int i; public boolean less(OrdInt o) {return i < o.intValue{} } The class OrdInt *doesn't* implement Ord. If we try public boolean less(Ord o) {return i < o.intValue{} this doesn't work either - we lose our static type checking. Correct pizza version uses an F-bound. MORE ON UNIVERSAL AND EXISTENTIAL QUANTIFICATION IN TYPES Example in pizza paper: exists a . List this describe the type of a list where we didn't know the element type Existential types used often to model information hiding