Coding braindump
About Posts Tools OSSU Tags
Coding braindump

Programming Languages C - Week 3

A key source of expressiveness in ML’s type system (not rejecting too many programs that do nothing wrong and programmers are likely to write) is parametric polymorphism, also known as generics. We should also study static types of OOP languages, such as Java. The main thing we want to prevent is “method missing” errors, i.e. sending a message to an object that has no method for that message. The source of type-system expressiveness most fundamental to OOP is subtype polymorphism also known as subtyping.

A Made-Up Language of Records

To study the basic ideas behind subtyping, we will use records with mutable fields, as well as functions and other expressions. For records, we will have expressions for making records, getting a field and setting a field:

  • In the expression {f1=e1, f2=e2, ..., fn=en}, each fi is a field name and each ei is an expression. 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 is just a collection of fields, where each field has a name and a content.
  • For the expression e.f, we evaluate e to a value v. If v is a record with an f field, then the result is the 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 f field, then we update the f fields.

Now we need a type system, with a form of types for records and typing rules for each of our expressions. Like in ML, write record types as {f1:t1, f2:t2, ..., fn:tn}. E.g. {x:real, y:real} would describe records with two fields named x and y that hold contents of type real. Type-check expressions as follows:

  • If e1 has type t1, e2 has type t2 etc. then {f1=e1, f2=e2, ..., fn=en} has type {f1:t1, f2:t2, ..., fn:tn}
  • If e1 has a record type containing f:t and e2 has type t, then e1.f = e2 has type t.
  • If e has a record type containing f:t then e.f has type t.

Assuming the “regular” typing rules for other expressiones like variables, functions, arithmetic and function calls an example like this will type-ceck 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 function types with the same syntax as in ML.

Wanting Subtyping

However, 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 fice : real = distToOrigin(c)

The program is safe, but the type-checker would not let the program run. A natural idea is to make the type system more lenient as follows: If some expression has a record type {f1:t1, ..., fn:tn} then let the expression also have a type where some of the fields are removed. Then our example will type-check. This idea is called subtyping.

The Subtyping Relation

Adding subtyping to our made-up language will require adding only two things:

  • The idea of one type being a subtype of another: we will write t1 <: t2 to mean t1 is a subtype of t2
  • One new typing rule: if e has type t1 and t1 <: t2, then e also has type t2.

So we have separated the idea of subtyping into a single binary relation that we can define separately from the rest of the type system.

For subtyping the key guiding principle is substitutability. If we allow t1 <: t2 then any value of type t1 must be able to be used in every way a t2 can be.

We can now add four subtyping rules to our language to accept more valid programs:

  • “Width” subtyping: A supertype can have a subset of fields with the same types, i.e. a subtype can have “extra” fields.
  • “Permutation” subtyping: A supertype can have the same set of fields in a different order.
  • Transitivity: if t1 <: t2 and t2 <: t3 then t1 <: t3
  • Reflexivity: Every type is a subtype of itself: t <: t

Depth Subtyping

Atm there is no way for a supertype to have a field with a different type than in the subtype. E.g. conside this example which passes a “sphere” to a function expecting a circle:

fun circleY (c:{center:{y: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)

The type of circleY is {center:{x:real,y:real}, r:real}->real and the type of sphere is {center:{x:real,y:real,z:real}, r:real}, so the call circleY(sphere) can type-check only if

{center:{x:real,y:real,z:real}, r:real} <: {center:{x:real,y:real}, r:real}

This does not hold with our rules so far: we cannot “reach into a field to do subtyping”. The natural rule to add here is “depth” subtyping for records:

  • If ta <: tb then {f1:t1, ..., f:ta, ..., fn:tn} <: {f1:t1, ..., f:tb, ..., fn:tn}

This lets the above program typecheck. Unfortunately this rule breaks our type system, allowing programs that we do no want to allow to typecheck:

fun setToOrigin (c:{center:{x:real,y:real}, r:real})=
    c.center = {x=0.0, y=0.0}

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 _ = setToOrigin(sphere)
                                                    val _ = sphere.center.z

This program typechecks, but when we run the program, the last line will not work. The moral of the story: In a language with records with getters and setters, depth subtyping is unsound.

If, however a field is not settable (i.e. immutable), then the depth subtyping rule is sound and useful.

Function Subtyping

The rules for this are even less intuitive, but just as important. When we talk about function subtyping, we are talking about using a function of one type in place of a function of another type. For example if f takes a function g of type t1->t2, can we pass a function of type t3->t4 instead? If t3->t4 is a subtype t1->t2 then this is allowed because of the rules established above.

To understand function subtyping, let’s use this example of a higher-order function, which computes the distance between two-dimensional point p and the result of calling f with p:

fun distMoved (f : {x:real,y:real}->{x:real,y:real},
               p : {x:real,y:real}) =
    let val p2 : {x:real,y:real} = f p
        val dx : real = p2.x - p.x
        val dy : real = p2.y - p.y
    in Math.sqrt(dx*dx + dy*dy) end

The type of distMoved is

(({x:real,y:real}->{x:real,y:real})*{x:real,y:real}) -> real

So a call to distMoved requiring no subtyping could look like this:

fun flip p = {x=~p.x, y=~p.y}
val d = distMoved(flip, {x=3.0,y=4.0})

The call could also pass in a record with extra fields, such as {x=3.0,y=4.0,color="green"}, but this is just ordinary width subtyping on the second argument to distMoved. We are interested in seeing whether functions with types other than {x:real,y:real}->{x:real,y:real} can be passed for the first argument to distMoved.

First, it is safe to pass in a function that “promises” more, i.e. returns a subtype of the needed return type for the function {x:real,y:real}. E.g. it is fine for this call to type-check:

fun flipGreen p = {x=~p.x, y=~p.y, color="green"}
val d = distMoved(flipGreen, {x=3.0,y=4.0})

The type of flipGreen is {x:real,y:real}->{x:real,y:real,color:string}. This is safe because flipGreen is substitutable for values of the type distMoved expects.

In general, the rule here is that if ta <: tb then t -> ta <: t -> tb. Return types are covariant for function subtyping.

Now consider passing in a function with a different argument type. Consider this:

fun flipIfGreen p = if p.color = "green"
                    then {x=~p.x,y=~p.y}
                    else {x=p.x, y=p.y}
val d = distMoved(flipIfGreen, {x=3.0, y=4.0})

The type of flipIfGreen is {x:real,y:real,color:string} -> {x:real,y:real}. This program should not type-check. If we run it, the expression p.color will have a “no such field” type error since the point passed does not have a color field.

But it works fine to use a function that needs “less arguments” in place of another function:

fun flipX_YO p = {x=~p.x, y=0.0}
val d = distMoved(flipX_YO, {x=3.0,y=4.0})

The type here is {x:real}->{x:real,y:real}, the call to distMoved causes no problems. The treatment of argument types for function subtyping is contravariant, i.e. if tb <: ta, then ta -> t <: tb -> t.

As a final example, function subtyping can allow contravariance of argumentsa and covariance of results:

fun flipXMakeGreen p = {x=~p.x, y=0.0, color="green"}
val d = distMoved(flipXMakeGreen, {x=3.0,y=4.0})

The type of flipXMakeGreen is {x:real} -> {x:real,y:real,color:string}, which is a subtype of {x:real,y:real} -> {x:real,y:real}, because {x:real,y:real} <: {x:real} (contravariance on arguments and {x:real,y:real,color:string} <: {x:real,y:real} (covariance on results).

The general rule for function subtyping is: If t3 <: t1 and t2 <: t4 then t1->t2 <: t3->t4.

Subtyping for OOP

An object is basically a record holding fields and methods. We assume the “slots” for methods are immutable: if an object’s method m is implemented with some code, there is no way to mutate m. Sound subtyping follows these rules then:

  • A subtype can have extra fields
  • Because fields are mutable, a subtype cannote have a different type for a field
  • A subtype can have extra methods
  • Because methods are immutable, a subtype can have a subtype for a method, which means the method in the subtype can have contravariant argument types and a covariant result type.

However, object types in Java and C# do nto look like record types and function types. E.g. we cannot write down a type that looks sth like this:

{fields : x:real,y:real,...
                            methods: distToOrigin : () -> real,...}

Instead, we reuse class names as types where if there is a class Foo, the the type foo includes in it all fields and methods implied by the class definition (including superclasses). Interfaces are more like record types, except they do not include fields. These are the rules for subclasses:

  • a subclass can add fields but not remove them
  • a subclass can add methods but not remove them
  • A subclass can override a method with a covariant return type
  • a class can implement more methods than an interface requires or implement a required method with a covariant return type.

Generics versus Subtyping

We have now studied subtype polymorphism (subtyping) and parametric polymorphism (aka generics). Let us now compare the two:

Generics are used by many programming idioms. There are functions that combine other functions such as compose:

val compose : (`b -> `c) * (`a -> `b) -> (`a -> `c)

Second, there are functions that operate over collections/containers where different collections/containers can hold values of different types:

val length : `a list -> int
val map : (`a -> `b) -> `a list -> `b list
val swap : (`a * `b) -> (`b * `a)

The key point is that if we had to pick non-generic types for these functinos, wwe would end up with less code reuse. E.g. we would need one swap function for producing an int * bool from a bool * int and another swap for swapping an int * int.

The type of swap indicates that the second component of the result has the same type as the second component of the argument.

Subtyping is a bad substitute for generics

Writing generic code in terms of subtyping instead of generics is painting with a hammer instead of a paintbrush: possible, but wrong. Consider this Java example:

class LamePair {
    Object x;
    Object y;
    LamePair(Object _x, Object _y){x=_x; y=_y; }
    LamePair swap() {return new LamePair{y,x}; }
    ...
}

String s = (String)(new LamePair("hi",4).y);  //error caught only at run-timeu

The code in LamePair type-checks w/o problem: the fields x and y have type Object, which is a supertype of every class and interface. The difficulties arise when using the class. Passing args to the constructor works as expected with subtyping. But when we retrieve the contents of a field, getting an Object is not very useful: we want the type of value we put back in.

Subtyping does not work that way: the type system knows only that the field holds an Object. So we have to use a downcast, e.g. (String)e, which is a run-time check that the result of evaluating e is actually of type String or a subtype thereof. SUch checks have the usual dynamic-checking costs in terms of performance and failure. In the example above the downcast would fail: it is the x field that holds a String not the y field.

What is subtyping good for?

Subtyping is great for allowing code to be reused with data that has “extra information”. E.g. geometry code that operates over points should work fine for colored points. It is certainly inconvenient in such situations that ML code like this simply does not type-check:

fun distToOrigin1 {x=x,y=y} =
    Math.sqrt (x*x + y*y)

              (*does not type-check*)
              (* val five = distToOrigin1 {x=3.0,y=4.0,color="red"} *)

Subtyping works very well for GUIs - much of the code for graphics libraries works fine for any sort of graphical element (“paint it on the screen”, etc.) where different elements such as buttons, bars, text boxes can be subtypes.

Generics are a bad substitute for subtyping

In a language with generics instead of subtyping you can code up your own code reuse with higher-order functions, but it can be a lot of trouble for a simple idea:

fun distToOrigin2(getx,gety,v) =
    let
        val x = getx v
        val y = gety v
    in
        Math.sqrt (x*x + y*y)
    end

fun distToOriginPt (p : {x:real,y:real}) =
    distToOrigin2(fn v => #x v,
                  fn v => #y v,
                  p)


fun distToOriginColorPt (p : {x:real,y:real,color:string}) =
    distToOrigin2(fn v => #x v,
                  fn v => #y v,
                  p)

Nonetheless w/o subtyping it may sometimes be worth writing code like this if you want it to be more reusable.

Bounded Polymorphism

There is no reason why a statically typed programming language cannot have generic types and subtyping. There are some complications from having both that we will not disuss (e.g. static overloading and subtyping are more difficult to define), but there are also benefits. We can combine the ideas to get even more code reuse and expressiveness.

The key idea is to have bounded generic types, where instead of just saying a “subtype of T” or “for all types `a”, we can say “for all types `a that are a subtype of T”. Like with generics, we can then use `a multiple times to indicate where two things must have the same type.

Consider this Point class in java with a distance method:

class Pt {
    double x, y;
    double distnace (Pt pt) { return Math.sqrt((x-pt.x)*(x-pt.x)+(y-pt.y)*(y-pt.y)); }
    Pt(double _x, double _y) { x = _x; y = _y; }
}

Now consider this static method that takes a list of points pts, a point center and a radius and returns a new list of points containing al the input points within radius of center, i.e. within the circle defined by center and radius:

static List<Pt> inCircle(List<Pt> pts, Pt center, double radius) {
    List<Pt> result = new ArrayList<Pt>();
    for (Pt pt : pts)
        if(pt.distance(center) <= radius)
            result.add(pt) ;
    return result;
}

This code works perfectly fine for a List<Pt>, but if ColorPt is a subtype of Pt, then we cannot call inCircle method above with a List<ColorPt> argument. Even if it were we would like to have a result type of List<ColorPt> when the argument type is List<ColorPt>. Java’s bounded polymorphism lets us describe this situation:

static <T extends Pt> List<T> inCircle(List<T> pts, Pt center, double radius) {
    List<T> result = new ArrayList<T>();
    for (T pt : pts)
        if(pt.distance(center) <= radius)
            result.add(pt);
    return result;
}

This method is polymorphic in type T, but T must be a subtype of Pt.