• An example to start off
• System F (Girard|Reynolds)
• Polymorphism
  • Parametric Polymorphism
    • Some examples
• Existential Type
  • A Example

First we have the following two examples of recursive functions

func toStrings(L: int list) string list = 
   case l of
      [] => []
      | x::xs =>
         IntToString(x)::toStrings(xs)

func add(l: int list, a: int) int list = 
   case l of
      [] => []
      | x::xs => (a+x)::add(xs,a)

We can have a more general function as the following

map: for all a and b, (a->b)->a list -> b list
fun map f l = 
   case l of
      [] => []
      | x::xs => f(x)::map[a][b](xs)

It is called polymorphism generality.

To achieve these, we need variables in type: we have the following judgement

$Deltavdashtau type$
where $Delta$ means $t_1 type,…,t_n type$

Take the map function as an example:

$$a type,b typevdash(arightarrow b)rightarrow a listrightarrow b list type$$

It reads as: $(arightarrow b)rightarrow a listrightarrow b list$ is a type
assuming that $a$ is a type and $b$ is a type.

The inference rule for that

$$frac{Deltavdashtau type;Deltavdashsigma type}{Deltavdashtaurightarrowsigma type}$$
$$frac{Delta,t typevdashtau type}{Deltavdashforall t.tau type}$$

System F (Girard|Reynolds)

The idea is: allow $lambda$ and application for type variables

$$frac{Delta,t type;Gammavdash e:tau}{Delta,GammaLambda t.e:forall t.tau}$$

(With function $rightarrow$)

Application rule:

$$frac{Delta,Gammavdash e:forall t.tau;Deltavdashsigma type}{Delta,Gammavdash e[sigma]:[sigma/t]tau}$$

(We use capital lambda $Lambda$ as oppose to $lambda$ just to distinguish the fact
that this is a type variable but not a term variable)

Then map function would become

$$map=Lambda aLambda b.lambda f:(arightarrow b).lambda x:a list$$

The Dynamics:

$$frac{emapsto e'}{e[sigma]mapsto e'[sigma]}$$
$$frac{}{(Lambda.e)[sigma]mapsto[sigma/t]e}$$

Substitution rules:

$$If Delta,t typevdashtau type\ and Delta,t type;Gammavdash e:tau\ and Deltavdashsigma type\ then Delta,Gammavdash[sigma/t]e:[sigma/t]tau$$

Polymorphism

There are actually two kinds of polymorphism: Intensional, and Parametric

Intensional: Different code at different types (e.g. some case switch in the code says:
if type is int do this, if type is double do that, …) (more programs)

Parametric: Same code at many types (e.g. map function above) (more theorems)

Parametric Polymorphism

We can infer more just from the types if something is parametric polymorphic.

Take some examples to see what can we say about any function of the type

Some examples

$forall aforall b, (arightarrow b)rightarrow a list rightarrow b list$

Every element of the result list must be $f(x)$ for some $x:a$) in the input list!!!

$r:forall aforall b, a listrightarrow a list$

All a’s in output must come from input!!!

Note: if we are writing a specific function of specific type $int listrightarrow int list$,
it could include something in the output that’s not in the input.

From the above $r$ function with it’s type, and the map function definition above (not just the type!),
for any $f:taurightarrowsigma$, and any $l:tau list$:

$$map f(r[tau]l)=r[sigma](map fl)$$

Existential Type

This adds nothing to System F, though it can actually be derived from System F

$$frac{Delta,t typevdashtau type}{Deltavdashexists t.tau type}$$
$$frac{Deltavdashsigma type;Delta,Gammavdash e:[sigma/t]tau} {Delta,Gammavdash pack[sigma]e:exists t:tau}$$

Application:

$$frac{Delta,Gammavdashsigma type;Delta,Gammavdash e_1:exists t.tau;Delta,t type,Gamma,x:tauvdash e:sigma} {Delta,Gammavdash open(t,x)=e_1 in e:sigma}$$

It corresponds to modules/abstract/private/hidden types. We want to draw boundaries
between the implementation and the clients that use it, via some abstract types.
i.e. interface!

A Example

$underline{Counter}$:

$$% <![CDATA[ exists t:<zero hookrightarrow t,Incrhookrightarrow trightarrow t,valuehookrightarrow trightarrow nat> %]]>$$

We can have two implementations of this:

(1) Take $t$ to be $nat$ (unary)

$$zero=0\ Incr(x)=s(x)\ value(x)=x$$

in which case

$$% <![CDATA[ pack[nat]\ <zerohookrightarrow 0,Incrhookrightarrowlambda x.s(x),valuehookrightarrowlambda x.x> %]]>$$

(2) Take $t$ to be $list(bit)$ (binary)

$$% <![CDATA[ pack[list(bit)]\ <zerohookrightarrow[0],\ Incrhookrightarrow func incr []=[1]|incr(0::bs)=1::bs|incr(1::bs)=0::incr(bs)\ valuehookrightarrowlambda bs.Sigma 2^i*nth bs i> %]]>$$

Now we have two kinds of implementation of the same interface!

A client of $underline{Counter}$ looks like:

$open(c,<zero,incr,value>)=$

some impl (unary/binary) in some code that uses $zero:c,incr:crightarrow c,value:crightarrow nat$

Note: the abstract type doesn’t escape the $open$

Note: the unary counter(UC) impl should be observational equivalent to the binary counter(BC),
which means no client can distinguish between them, if

1. client only uses exposed operations
2. implementation are obs eqv. (i.e. they behave the same)

Key idea: choose a “simulation” relation between UCs and BCs that is preserved by the operations

1. UC zero is related to BC zero
2. UC incr is related to BC inc
3. UC value is related to BC value