CSE 505 -- Very Rough Notes on F-Bounded Polymorphism

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