Inhalt

Beachte: Material teilweise auf Deutsch und Englisch.

Polymorphie in C++ (Motivation)

Polymorphie (griechisch Vielgestaltigkeit) ist ein Programmierkonzept. Zweck: Einheitliche Schnittstelle welche auf verschiedene Typen anwendbar ist. Es gibt verschiedene Formen von Polymorhpie:

• Subtypen Polymorphie

• Parametrische Polymorphie (aka “generics”)

• Ad-hoc Polymorphie (aka “overloading”)

Unten finden sich eine Reihe von C++ Beispielen.

#include <stdio.h>

/////////////////////////
// Subtype polymorphism

// Coercions
int func(float x) {
    if (x < 1.0) return 1;
    return 0;
}

void testCoerce() {
 int arg = 1;
 float res;

 res =func(arg);
}


// Nominal subtyping
class Point {
public:
  int x,y;
};

class ColoredPoint : public Point {
public:
  int colorCode;
};

void printPoint(Point p) {
    printf("\n x = %d y = %d", p.x, p.y);
}

void testPoint() {
  ColoredPoint cp;
  printPoint(cp);
}


// Vererbung + virtuelle Methoden
class Shape {
public:
  virtual int area() = 0;
};


class Square : Shape {
  int x;
public:
  Square (int _x) { x = _x; }
  int area() { return x * x; }
};

class Rectangle : Shape {
  int x,y;
public:
  Rectangle(int _x, int _y) { x = _x; y = _y; }
  int area() { return x * y; }
};


///////////////////////////////
// Ad-hoc polymorphism

// Ueberladung


void mySwap2(int& x, int& y) {
  int tmp;
  tmp=x; x=y; y=tmp;
}

void mySwap2(Point& x, Point& y) {
  Point tmp;
  tmp=x; x=y; y=tmp;
}

void testSwap2() {
  int x, y;

  mySwap2(x,y);

  Point p;
  ColoredPoint cp;

  mySwap2(p,cp);

}


///////////////////////////////
// Parametric polymorphism

// Templates
template<typename T>
void mySwap(T& x, T& y) {
  T tmp;
  tmp=x; x=y; y=tmp;
}


void testSwap() {
  int x, y;

  mySwap<int>(x,y);

  Point p;
  ColoredPoint cp;

  mySwap<Point>(p,cp);

}


int main() {

   return 0;
}

Subtype polymorphism

Idea:

S is a subtype of T, usually written as $S \leq T$.

A value of type $S$ can also be used at a place where a value of type $T$ is expected.

Coercive subtyping (compile-time instrumentation)

• Suppose we have a function of type Float -> Int.

• It should be safe to pass as an argument a value of type Int and store the resulting value in a variable of type Float.

• In C-style pseudo code:

int func(float x) {
    if (x < 1.0) return 1;
    return 0;
}

int main() {
 int arg = 1;
 float res;

 res = func(arg);
}

• The point is that in the above described situation, the function of type Float -> Int behaves like a function of type Int -> Float.

• This is safe, because we can safely coerce the integer argument into floating-point value. The same applies to the return value.

Instrumentation

Coercion a value of type Int into a value of type Float implies a change in (data) representation. The actual value remains unchanged however.

A standard method is to instrument the program based on the program’s typing. Assuming we have a function coerce : Int -> Float, instrumention of the above program yields.

int main() {
 int arg = 1;
 float res;

 res = coerce(func(coerce(arg)));
}

Insertion of the coercion is guided by the subtyping rule.

We write

G |- e : t --> E

to denote a source program e with type t where E is the instrumented program.


Similar to typing rules, we require rules that tell us how to build coercions.

We write

  |- t1 <= t2 --> c

to denote that t1 is a coercive subtype of t2 where c is the coercion function.


(ItoF)   |- Int <= Float --> coerce1

(FtoD)   |- Float <= Double --> coerce2


           |- t1 <= t2 --> c1     |- t2 <= t3 --> c2
(Trans)  ------------------------------------------
           |- t1 <= t3 -> c2 . c1

where c2 . c1 denotes function composition and
is equivalent to  \x -> c2(c1(x))


The coercive subtyping rule is as follows.

              G |- e : t1 --> E    |- t1 <= t2 --> c
(CoerceSub)  --------------------------------------
              G |- e : t2 --> c(E)

Nominal subtyping

Types in subtype relation must be declared explicitely. See for example (sub)class declarations in Java and C++.

class Point {
  public:
  int x,y;
};

class ColoredPoint : Point {
  public:
  int colorCode;
};

We have that ColoredPoint <= Point. So, anywhere where a Point object is expected, we can also use an object of type ColoredPoint.

Structural subtyping

Consider

class Point {
  public:
  int x,y;
};

class ColoredPoint : Point {
  int colorCode;
};

class CPoint {
  public:
  int x, y, colorCode;
};

Objects of type ColoredPoint and CPoint are structurally equivalent. Every entry in CPoint is also found in ColoredPoint and vice versa. So, Point is a structural subtype of CPoint.

Behavioral subtyping (aka Liskov substitution principle = LSP)

An expression $e$ is of type $t_1$ is a behavioral subtype of $t_2$, written $t_1 \leq t_2$, then $e$ can be used in any context where its expected type is $t_2$ without changing the behavior of the program.

Inheritance (run-time look-up of virtual methods)

Reuse of an existing implementation (method) and possibly override an existing implementation in a derived class.

Various forms of inheritance:

• Single versus multiple inheritance

• Static versus virtual methods

In general, LSP is no longer satisfied. Consider

// Pseudo code
class Bird {
  void fly() { ... }
}

class Eagle : Bird {
  void fly() { ... }
}

class Penguin : Bird {
  void fly() { ... } // can NOT fly !!!
}


func(Bird b) {
    b.fly();
}

main() {
  Bird b;
  Eagle e;
  Penguin p;
  func(b);
  func(e);
  func(p);    // behavior changes!

}

To guarantee LSP, need to impose stronger conditions (often formalized via “contracts”), or we can restrict the language. For example, in C++, if we only use static methods, LSP is guaranteed.

Strictly speaking, inheritance and subtyping are different concepts (but often they coincide).

Subtyping = subtype compatability, use an expression of subtype instead.

Inheritace = reuse of implementations.

In languages such as C++ and Java, subtypig can be expressed in terms of inheritance.

Function subtyping

Recall

int func(float x) {
    if (x < 1.0) return 1;
    return 0;
}

int main() {
 int arg = 1;
 float res;

 res = func(arg);  // P
}

• We find func : float -> int.

• At program point P, func is used in the context int -> float.

• So, we can argue that float -> int <= int -> float.

Subtyping among function in general:

• $t_1 \rightarrow t_2 \leq s_1 \rightarrow s_2$ iff

  1. $s_1 \leq t_1$, and
  2. $t_2 \leq s_2$.

We say, functions are contra-variant in the argument and co-variant in the result.

Pointer subtyping

• $t* \leq s*$ if $t \leq s$

We say that pointer subtyping is co-variant.

Array subtyping

Consider

class Point {};

class ColoredPoint : Point {};

class BlackWhitePoint : Point {};

Suppose array subtyping is co-variant.

• We find that ColoredPoint $\leq$ Point and BlackWhitePoint $\leq$ Point.

• Hence, we can follow:

  • ColoredPoint[] $\leq$ Point[]
  • BlackWhitePoint[] $\leq$ Point[]

• We further assume that ColoredPoint and BlackWhitePoint are not compatible (not in subtype relation)

• There’s a “writing” problem:

  • We turn an array of ColoredPoints into a Points array.
  • We fill (overwrite) an element in this array with a BlackWhitePoint
  • This leads to a crash (because ColoredPoint and BlackWhitePoint are not compatible)

Suppose array subtyping is contra-variant.

• Point[] $\leq$ ColoredPoint[]

• There’s again a “reading” problem:

  • We access an element and think it’s a ColoredPoint where in fact we only have a Point.
  • This leads to a crash.

Conclusion: Arrays ought to be invariant.

Array subtyping in Java

Array subtyping in Java is co-variant!

Hence, the following program is well-typed and will crash!

void main() {
String[] s;
s = new String[10];
test(s);
}

void test (Object [] a) {
  a[1] = new Point(10,20); // Crash!
}

OK, the crash leads to an exception, still, didn’t we just learn that array subtyping ought to be invariant?

Well, thanks to co-variant subtyping we can supply the programmer with “generic” array operations. We are using Object to mimic genericity here.

These operations are safe as long as we only read but not write (recall the earlier reasoning for invariance of array subtyping).

Of course, even co-variant array subtyping is safe due to run-time checks (we might encounter an exception).

Parametric polymorphism

A form of polymorphism where a function is implemented without mention of any specific type, i.e.~the implementation is parametric. The function will behave the same for specific instances.

C++

What about templates in C++?

template<typename T>
void swap(T& x, T& y) {
  T tmp;
  tmp=x; x=y; y=tmp;
}

• Templates are syntactic macro language which is expanded at compile-time.

• The expanded code is type-checked and compiled!

Some examples.

#include <iostream>

using namespace std;

// class template
template<typename T>
class Elem {
  T x;
public:
  Elem() {}
  Elem(T y) { x = y; }
  void replace(T y) { x = y; }
  T get() { return x; }
};


// function template
template<typename T>
void mySwap(T& x, T& y) {
  T tmp;
  tmp=x; x=y; y=tmp;
}


// template instantiation
int main() {
  Elem<int> i = Elem<int>(1);
  Elem<int> i2 = Elem<int>(2);
  Elem<char> c = Elem<char>('a');

  i.replace(3);

  mySwap<Elem<int> >(i,i2);
  // Because of T tmp in mySwap,
  // we need to provide the parameterless constructor in the Elem class

  // in some cases, template instances can be inferred by the compiler
  mySwap(i2, i);


  int j, j2;
  j = 1; j2 = 3;

  mySwap<int>(j, j2);
  mySwap(j2, j);

  return 1;
}

Compiler generates

class Elem_int {
  int x;
public:
  Elem_int() {}
  Elem_int(int y) { x = y; }
  void replace(int y) { x = y; }
  int get() { return x; }
};

class Elem_char {
  char x;
public:
  Elem_char() {}
  Elem_char(int y) { x = y; }
  void replace(char y) { x = y; }
  char get() { return x; }
};

void mySwap_Elem_int(Elem_int& x, Elem_int& y) {
  Elem_int tmp;
  tmp=x; x=y; y=tmp;
}

void mySwap_int(int& x, int& y) {
  int tmp;
  tmp=x; x=y; y=tmp;
}



int main() {
  Elem_int i = Elem_int(1);
  Elem_int i2 = Elem_int(2);
  Elem_char c = Elem_char('a');

  i.replace(3);

  mySwap_Elem_int(i,i2);
  // Because of T tmp in mySwap,
  // we need to provide the parameterless constructor in the Elem class

  // in some cases, template instances can be inferred by the compiler
  mySwap_Elem_int(i2, i);


  int j, j2;
  j = 1; j2 = 3;

  mySwap_int(j, j2);
  mySwap_int(j2, j);

  return 1;
}

Further note.

• Templates are vaguely connected to parametric polymorphism but it’s something different.

• If you’re interested, check out the “Concepts” discussion where some brave people try to enrich C++ with some “real” polymorphism.

The code duplication approach is fairly simply to implement via a type-directed translation scheme. There are some issues:

• There’s no separate compilation of template code (hence, template code needs to be put into the header file).

• Code duplication may lead to a blow-up of the resulting size of programs.

• Calls (recursive) on more specific types may be an issue.

Consider the contrived example.

func foo<T>(x T, xs []T, i int) [] T {
 if i > 0 {
   foo<[]T>(xs, [xs], i-1)               // Requires instance on lists !!!
 }
 xs[i] = x
 return xs
}

The “code duplication” approach will not work here.

Java

Java generics use a universial representation based on the Object type. That is, after compile-time type checking, polymorphic types are erased and can therefore not be inspected at run-time. This leads to a few restrictions. For example,

<T> T instantiateElementType(List<T> arg) {
     return new T(); //causes a compile error
}

yields a compile-time error because the type T necessary to build the object is unknown at run-time.

Aside: The “costly” coercion issue not a problem in the Java setting. We can cast any object into Object. For the other direction, we apply a type cast which is safe due to compile-time checking.

But polymorphic array creation is not possible in case of a homogenous translation of polymorphic code.

static Object[] foo(Object a) {
  Object[] ob = new Object[1]
  ob[0] = a
}
...
Integer i = new Integer(1)
Integer[] iArr = (Integer[])foo(i) //not possible

Full type inference

C++/Java require the programmer to explicitly annotate the program text with

• generic (in C++ template) type parameters, e.g. at class/function declaration sites, and

• instances at use sites.

Languages such as OCaml and Haskell support full type inference in the presence of parametric polymorphismn.

• (Parametric) types are automatically inferred.

• At use sites, the compiler automatically infers the required instance.

Here’s an example in Haskell.

apply f x = f x

What’s the type of apply?

Possible types are

apply :: (Int -> Int) -> Int -> Int
apply :: (Int -> Char) -> Int -> Char
...

Is there a most general type? Yes, there is!

apply :: (a -> b) -> a -> b

Some use cases.

test1 = apply (\x -> x) True

test2 = apply not False

test3 = apply head [1,2,3]

Parametric polymorphic type system

We take a look at the typing theory behind ‘generics’. For further details, see this great book Types and Programming Languages.

Formally, this is know as parametric polymorphism. The term polymorphism comes from greek and roughly stands for “many forms/shapes”. We have already seen subtyping polymorphism.

Let’s start with a classic example. What type should we give a sorting function?

For example, in OCaml we find

let apply f x = f x;;
val apply : ('a -> 'b) -> 'a -> 'b = <fun>

• The first argument is a function of type ('a -> 'b) which will be applied to the second argument of type 'a.

• The argument type of the function matches the type of the second argument.

• The definition of apply does not constraint 'a and 'b in any way.

• We say that 'a and 'b are parametric variables.

Java and C++

There are plenty of Generics Java examples. Please check the literature.

What about templates in C++?

template<typename T>
void swap(T& x, T& y) {
  T tmp;
  tmp=x; x=y; y=tmp;
}

• Templates are syntactic macro language which is expanded at compile-time.

• This is vaguely connected to parametric polymorphism but it’s something different.

• If you’re interested, check out the “Concepts” discussion where some brave people try to enrich C++ with some “real” polymorphism.

Parametric polymorphism typing rules

 e ::= x | \x->e | e e | let x = e in e
 t ::= t -> t               Function types
    |  Int                  Primitives
    |  Bool
    |  a                    Type variable
 sigma ::= t                    Simple type
         | forall a1 ... an. t  Quantified type
 G ::= G cup G | { x:sigma }    Variable environment


(Var)   (x:sigma) in G
       ------------
        G |- x : sigma

(App)   G |- e1 : t1 -> t2  G |- e2 : t1
        --------------------------------
        G |- e1 e2 : t2

(Abs)   G cup { x: t1 } |- e : t2
        -------------------------
        G |- \x->e : t1 -> t2

(Forall-Intro)  G |- e : t
                {a1, ..., an} in fv(t)
                {a1, ..., an} not in fv(G)
                ----------------------------
                G |- e : forall a1 ... an. t

(Forall-Elim)   G |- e : forall a1 ... an. t
                ----------------------------
                G |- e : [t1/a1, ..., tn/an] t

(Let)  G |- e1 : sigma
       G cup { x:sigma } |- e2 : t
       -------------------------
       G |- let x = e1 in e2 : t

• As before, each lambda abstraction introduces a distinct variable. The same applies to let definitions.

• Subtle point, we only quantify over simple types. Higher-rank polymorphism will not be discussed here.

• The above system is also known as the Hindley/Milner system aka rank-1 parametric polymorphic lambda calculus with a let construct.

• The rank indicates the nesting of quantifiers. In our case, rank 1 states that quantifiers only appear at the outermost level.

Auxilliary definitions

Free variables

fv(t) denotes the set of free variables in t.
We define fv(t) by structural induction:

fv(Int)     = {}
fv(Bool)    = {}
fv(a)       = {a}
fv(t1->t2)  = fv(t1) cup fv(t2)

In case of a type scheme, the free variables equal all free type variables
but those which are quantified.

fv(forall a1 ... an.t) = fv(t) - {a1,...,an}


The free variables in environment G equal the free variables of the types of variables.

fv({})              = {}
fv({ x : sigma})    = fv(sigma)
fv(G1 cup G2)       = fv(G1) cup fv(G2)

Type instantiation

We say t is an instance of sigma if t can be derived from sigma by instiation of free type variables.
We write sigma <= t in such a case.
The formal definition of sigma <= t is as follows.

sigma <= sigma           a type is an instance of it self



forall a1 ... an.t <= t'  iff  there exists t1 ... tn such that [a1 |-> t1,...,an |-> tn]t <= t'

Typing examples

Consider \x-> x y:

             (Var) {y : a1, x : a1->a2 } |- x : a1->a2
   (App)     (Var) {y : a1, x : a1->a2 } |- y : a1
           ---------------------------------------------------------
   (Abs)   {y : a1, x : a1->a2 } |- x y : a2
           --------------------------------------------
 (Forall-Intro)
           {y : a1} |- \x-> x y : (a1->a2) -> a2
           --------------------------------------------
           {y : a1} |- \x-> x y : forall a2. (a1->a2) -> a2

We can quantify over a2 but not a1.

Explicitly versus implicitly typed expression

• Suppose we have a well-typed expression e, that is, we have that G |- e : t for some environment G and type t.

• In Java/C++, expressions (programs) are explictly typed. That is, the type of each variable must be provided and in case of a generic expression applied in a specific context, the specialized type must be given.

template<typename T>
void swap(T& x, T& y) {
  T tmp;
  tmp=x; x=y; y=tmp;
}

int main() {

  int i=1, j=2;
  swap<int>(i,j);

  char c='a', d='b';
  swap<char>(c,d);
}

• Let’s extend our expression language and make type abstraction and type application explicit. In addition, we allow for the explicit annotation of types of lambda bound variables.

  We write /\ a -> for type abstraction, e.g. written in C++ as template<typename a>. We write e[t] for type application, e.g. written in C++ as e<t>.

 e ::= x | \x->e | e e | let x = e in e
    | \x:t-> e                                Type annoted abstraction
    |  /\ a -> e                              Type abstraction
    | e[t]                                    Type application
 t ::= t -> t               Function types
    |  Int                  Primitives
    |  Bool
    |  a                    Type variable
 sigma ::= t                    Simple type
         | forall a1 ... an. t  Quantified type
 G ::= G cup G | { x:sigma }    Variable environment

(Var)   (x:sigma) in G
       ------------
        G |- x : sigma

(App)   G |- e1 : t1 -> t2  G |- e2 : t1
        --------------------------------
        G |- e1 e2 : t2

(Abs)   G cup { x: t1 } |- e : t2
        -------------------------
        G |- \x->e : t1 -> t2

(Abs-Annot)   G cup { x: t1 } |- e : t2
              -------------------------
              G |- \x:t1->e : t1 -> t2

(Forall-Intro)  G |- e : t
                {a1, ..., an} in fv(t)
                {a1, ..., an} not in fv(G)
                ----------------------------
                G |- e : forall a1 ... an. t

(Forall-Elim)   G |- e : forall a1 ... an. t
                ----------------------------
                G |- e : [t1/a1, ..., tn/an] t

(Let)  G |- e1 : sigma
       G cup { x:sigma } |- e2 : t
       -------------------------
       G |- let x = e1 in e2 : t


(Ty-Abs)   G |- e : t     a in fv(t)   a not in fv(G)
          -------------------------------------------
           G |- /\ a -> e : forall a.t


(Ty-App)  G |- e : forall a.t1
          ------------------------------------
          G |- e[t2] : [t2/a] t1

Recall our earlier (implicitly) typed example \x-> x y:

             (Var) {y : a1, x : a1->a2 } |- x : a1->a2
   (App)     (Var) {y : a1, x : a1->a2 } |- y : a1
           ---------------------------------------------------------
   (Abs)   {y : a1, x : a1->a2 } |- x y : a2
           --------------------------------------------
 (Forall-Intro)
           {y : a1} |- \x-> x y : (a1->a2) -> a2
           --------------------------------------------
           {y : a1} |- \x-> x y : forall a2. (a1->a2) -> a2

Here’s the explicit variant /\ a2 -> \x:(a1->a2)-> x y:

             (Var) {y : a1, x : a1->a2 } |- x : a1->a2
   (App)     (Var) {y : a1, x : a1->a2 } |- y : a1
           ---------------------------------------------------------
 (Abs-Annot)  {y : a1, x : a1->a2 } |- x y : a2
             --------------------------------------------
 (Ty-Abs)
           {y : a1} |- \x:(a1->a2)-> x y : (a1->a2) -> a2
           a2 in fv((a1->a2) -> a2)   a2 not in fv({y : a1})
           --------------------------------------------
           {y : a1} |- /\ a2 -> \x:(a1->a2)-> x y : forall a2. (a1->a2) -> a2

Point to note. There is no more guessing involved once we strictly use explicitly typed expressions.

Fact. Every implicitly typed expression can be converted into an explicitly typed expression.

Extended example making use of the let construct:

let f = /\ a2 -> \x:(a1->a2)-> x y
in f[Int] z

where we assume G = {y : a1, z : a1->Int}.

Let’s consider the (explicit) typing derivation:

    (Ty-App) G' |- f : forall a2. (a1->a2) -> a2
            [Int/a2] ((a1->a2) -> a2)  = (a1->Int)->Int           (z : a1->Int)  in G'
            ------------------------------                 (Var) -------------------
 (App)      G'  |- f[Int] : (a1->Int)->Int                       G' |- z : a1->Int
       G' = G cup { f : forall a2. (a1->a2) -> a2 }
       -----------------------------------------------------------
 (Let) G cup { f : forall a2. (a1->a2) -> a2 } |- f[Int] z : Int
       G |- /\ a2 -> \x:(a1->a2)-> x y : forall a2. (a1->a2) -> a2 (see above)
      -------------------------------------------------------
      G |- let f = /\ a2 -> \x:(a1->a2)-> x y   : Int
           in f[Int] z

Some results

• Type inference for the Hindley/Milner system is decidable and yields most general type. This result is due to Damas/Milner (W algorithm published in 1985).

• The time complexity can be exponential (for mostly contrived examples).

• Type checking for the explictely typed variant is rather straightforward.

• Any implicitely typed program that is well-typed can be translated into an explicitely typed program.

Compilation of parametric polymorphism

Roughly, there are two possible approaches to compile programs which make use of parametric polymorphism.

1. Duplicate code for specific instantiations.

2. Avoid code duplication by using a universal representation of types.

The code duplication approach is fairly simply to implement via a type-directed translation scheme. There are two issues:

• Code duplication may lead to a blow-up of the resulting size of programs.

• Calls (recursive) on more specific types may be an issue.

In case of a universal representation of types we may require reflection to cast the universal type into a more specific type. This may imply some (possibly costly) coercions.

There are improvements to this compilation scheme. See for example

• Compiling Polymorphism Using Intensional Type Analysis by Harper and Morrisett

Java

Java generics use a universial representation based on the Object type. That is, after compile-time type checking, polymorphic types are erased and can therefore not be inspected at run-time. This leads to a few restrictions. For example,

<T> T instantiateElementType(List<T> arg) {
     return new T(); //causes a compile error
}

yields a compile-time error because the type T necessary to build the object is unknown at run-time.

Aside: The “costly” coercion issue not a problem in the Java setting. We can cast any object into Object. For the other direction, we apply a type cast which is safe due to compile-time checking.

But polymorphic array creation is not possible in case of a homogenous translation of polymorphic code.

static Object[] foo(Object a) {
  Object[] ob = new Object[1]
  ob[0] = a
}
...
Integer i = new Integer(1)
Integer[] iArr = (Integer[])foo(i) //not possible