# An example to start off

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

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

Take the `map`

function as an example:

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

The inference rule for that

# System F (Girard|Reynolds)

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

(With function $\rightarrow$)

Application rule:

(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

The Dynamics:

Substitution rules:

# 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 a\forall b, (a\rightarrow 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 a\forall b, a\ list\rightarrow a\ list$

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

Note: if we are writing a specific function of specific type $int\ list\rightarrow 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:\tau\rightarrow\sigma$, and any $l:\tau\ list$:

# Existential Type

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

Application:

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}$:

We can have two implementations of this:

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

in which case

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

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:c\rightarrow c,value:c\rightarrow\ 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

- client only uses exposed operations
- 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

- UC zero is related to BC zero
- UC incr is related to BC inc
- UC value is related to BC value