Types

Martin Sulzmann

Content

Type inference versus type checking
Typing rules and typing derivations
Type checking/inference in Go (and some design choices in Go)
Polymorphism
- Subtype polymorphism
- Parametric polymorphism
- Ad-hoc polymorphism
- Bounded polymorphism
- Inheritance versus subtyping
Dependent types

Type inference versus type checking

package main

import "fmt"

func main() {
    var x int
    x = 1
    y := x + 1
    fmt.Printf("y = %d", y)

}

The type of y is inferred by the right-hand side.

Pretty convenient!

Languages like Haskell support full type inference where the types of functions can be inferred.

Type inference refers to the process of automatically inferring the type of program text (variables, expressions, functions, ...).

Type checking refers to the process of automatically checking if the provided (user-annotated) type information matches the progrm text.

Sometimes, the term type inference used in a context where we only carry out type checking. Unless a clear distinction between inference and checking is necessary, we often use the (more general) term type inference instead of type checking.

Both methods can either be carried out statically (at compile-time) or dynamically (at run-time).

Both methods rely on typing rules that specify the conditions under which some program text is type correct. For example, for an assignment statement we demand that the types of the expressions of the left-hand and right-hand side must be identical. There is an entire branch of computer science devoted in the formalization of such typing rules and how to effectively implement via type checking/inference.

Typing rules and typing derivations

Why do we need formal typing rules?

Consider the informal typing rules for arithmetic expressions.

Every integer constant is of type int
An expression composed of addition is of type int if the left and right subexpressions are of type int.

The issue is that

there may be some ambiguities, and
we cannot mechanize the task of type checking.

We seek a formal system in which

we can concisely formalize typing rules, and
we can mechanize the task of type inference/checking.

We use a formal system represented by some typing rules. A typing rules makes statement about the well-typing of expressions. Expressions may contain free variables. So, we need to know the types of these variables.

We assume an environment G of the following form.

G denotes a set of type/variable declarations of the form
{x1 : int, ..., xn : int}

where x1, ..., xn are distinct.

We refer to xi : int as a type assignemt.

We write G |- e : int to denote that expression e has type int under the environment G. We refer to G |- e : int as a typing judgment.

We characterize all valid typing judgments in terms of typing rules.

      x : int is an element in G
(Var) -------------
      G |- x : int

       i is a natural number
(Int) ---------------
      G |- i : int

      G |- e1 : int     G |- e2 : int
(Add) ---------------------------------
      G |- e1 + e2 : int

Above to be read as "if-then" rules. The part above the --- is the precondition (premise) and the part below is the postcondition (conclusion).

We verify that { x:int, y:int } |- x + (y + 1) : int is valid (derivable) by building a typing derivation tree. The important obvservation is that all typing rules are syntax-directed. So, based on the syntax of expressions we can decide which typing rule to apply.

                                                y : int in { x:int, y:int }         1 is a natural number
                                          (Var) --------------------------  (Int) -------------------------
             x : int in { x:int, y:int }       { x:int, y:int } |- y : int       { x:int, y:int } |- 1 : int
    (Var) ---------------------------    (Add) -------------------------------------------------------------
         { x:int, y:int } |- x : int           { x:int, y:int } |- y + 1 : int
(Add) ---------------------------------------------------------------------------
       { x:int, y:int } |- x + (y + 1) : int

It is rather straightforward here to build the typing derivation tree. Assuming the expression is representd by some AST (= Abstract Syntax Tree), the type checker/inferencer simply needs to recurse over the AST (by structural induction) where for each kind of expression we have a checker/inference function that applies the respective typing rule.

Type checking/inference in Go (and some design choices in Go)

We take a brief look at type checking/inference in Go. Consider the following example.

package main

import "fmt"

func f(x int) int {
    var y int
    y = x + 1
    return y
}

func f2(x int) int {
    y := x + 1
    return y
}

func main() {
    var x int
    x = 1

    fmt.Printf("%d \n", f(x))
    fmt.Printf("%d \n", f2(x))
    g := f
    y := 1
    fmt.Printf("%d \n", g(y))

}

Via x := e we indicate that on the left-hand side we introduce (declare) a fresh variable x whose value is determined by the right-hand side e. No explicit type annotations are provided as the type of x can be determined by inferring the type of e.

How does this (simple) form of type inference work? We can assume that the types of all variables on the right-hand side is known. So, we check by following the typing rules of the right-hand side expression is type correct. As part of this type checking process, we also infer the expression's type.

For example, consider the expression from above.

x + 1

where x is of type int


We type check x + 1 as follows.

   We observe the structure of the expression.
   In our case, we find addition with x and 1 as operands.
   So rule (Add) from above applies.

   We can conclude that x + 1 is of type int if
   x is of type int and 1 is of type int.
   This holds!

   Notice something?
   By the way, we infer the type of x + 1!
   We traverse the structure of the expression (structural induction)
   by going from the outer level (addition) to the inner level (operands).

What is full type inference? If we could omit all type annotations. In Go we still need to provide of function definitions. In other languages, e.g. Haskell, the type of function definitions is optional. We say that such languages support full type inference.

Let's consider our running example where all type annotations are omitted.

func f3(x) {
   y = x + 1
   return y
}

Let's attempt to reconstruct the missing type annotations by inspection of the program text.

1. Consider x + 1
   Based on the above typing rules we deduce that
   x + 1 is of type int and therefore
   x is of type int as well.

2. Consider y = x + 1
   The types of left-hand and right-hand side must match.
   Hence, we deduce that y is of type int.

3. return y
   implies that f3's return type is int

Putting the pieces together, we deduce the following.

func f3(x int) int {
   var y int
   y = x + 1
   return y
}

Is that the only type we can give to this program text. Well, Go also supports float32. So, another possible annotation would be the following.

func f3(x float32) float32 {
   var y float32
   y = x + 1
   return y
}

The program text x + 1 typechecks under the assumption that the integer constant 1 can be coerced into a floating point number.

The above issue, several types that can be inferred, highlights one of the challenges of type inference. The quest is to design a programming language that enjoys principal type inference. By principal we mean, type inference yields a most general type that subsumes all other types. For more details on this subject, please refer to the research literature.

Coming back to Go. None of the above types inferred for f3 is better than the other type. Hence, depenending which type we choose (infer) we might reject some program. For a concrete example see below.

package main

import "fmt"

/*

Suppose Go supports full type inference

func f3(x) {
   y = x + 1
   return y
}

*/

// The following types can be inferred for f3.
// Both types are incomparable as depending which type we choose
// we might reject some program. See below.

func f3a(x int) int {
    var y int
    y = x + 1
    return y
}

func f3b(x float32) float32 {
    var y float32
    y = x + 1
    return y
}

func main() {
    var x, y int
    var f, g float32

    x = 1
    y = 1
    f = 1.0
    g = 1.0

    x = f3a(y) // OK
    // g = f3a(f) // NOT OK

    g = f3b(f) // OK
    // x = f3b(y) // NOT OK

    fmt.Printf("%d %d %f %f", x, y, f, g)

}

Polymorphism

Polymorphism ("greek)" = "many forms".

Polymorphism in programming languages: The ability that a function can be used on values of different types.

Various forms of polymorphism.

Subtype polymorphism
Parametric polymorphism
Ad-hoc polymorphism

Subtype polymorphism (aka inclusion polymorphism)

In general, if an expression $e$ is of type $t_1$ and $t_1$ is a 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$ .

 (Sub)   G |- e : t1  t1 <= t2
         ---------------------
         G |- e : t2

Let's take a look at some specific examples of this (subtyping) principle.

Coercive subtyping

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 {
  int x,y;
}

class ColoredPoint : Point {
  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 {
  int x,y;
}

class ColoredPoint : Point {
  int colorCode;
}

class CPoint {
  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

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

class A {
   int m1() { return 1; }
   bool m2() { return false; }
}

class B : A {
  int m1() { return 2; }
}

Various forms of inheritance:

Single versus multiple inheritance
Static versus virtual methods

In general, LSP is no longer satisfied. Consider

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 programpoint 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.

Array subtyping

Co-variant?

We assume 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)

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).

Recall function subtyping

Earlier we argued that the following ought to hold:

t1→t2≤s1→s2t_1 \rightarrow t_2 \leq s_1 \rightarrow s_2 iff
1. $s_1 \leq t_1$ , and
2. $t_2 \leq s_2$ .
What could possibly go wrong if we use the following variant where the argument as well as the result are co-variant:
- t1→t2≤s1→s2t_1 \rightarrow t_2 \leq s_1 \rightarrow s_2 iff
  1. $t_1 \leq s_1$ , and
  2. $t_2 \leq s_2$ .
Consider the following example.

class Point {
  int x,y;
}

class ColoredPoint : Point {
  int colorCode;
}

We have that ColoredPoint <= Point.

Assuming strictly co-variance, we find that ColoredPoint -> Int <= Point -> Int.

Let's define the following function

int extract(ColoredPoint cp) {
 return cp.colorCode;
}

extract has type ColoredPoint -> Int. Based on the subtyping principle and the fact that ColoredPoint -> Int <= Point -> Int, we can use extract in a context Point -> Int. That is, pass a value of type Point to extract.

Will this work? No!

If we pass a value of type Point to extract, in the function body we attempt to access the element colorCode which does not exist. Hence, we obtain some run-time failure.

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.

Parametric polymorphic type system

We take a look at the typing theory behind 'generics'.

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.

Duplicate code for specific instantiations.
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

Ad-hoc polymorphism

A form of polymorphism where a function can be applied to different types where the behavior may depend on the specific type instances, i.e.~the implementation is ad-hoc.

Method overloading in Go can be seen as a specific form of ad-hoc polymorphism.

Type classes (in Haskell)

data List a = Null | Cons a (List a)

member x Null = False
member x (Cons y ys)
    | x == y    = True
    | otherwise = member x ys

What's the type? Here's what type inference tells as (to be explained in more detail below).

*Main> :t member
member :: Eq a => a -> List a -> Bool

member works for any type
provided we supply an instance of (type) class Eq
== is an overloaded function (operator) which belongs to type class Eq

Part of the Haskell Prelude (i.e. already defined).

class Eq a where
 (==) :: a -> a -> Bool

A type class specifies the set of methods which shall be defined for this case. Eq t expresses that type t is a member of type class Eq and hence we can assume that overloaded method (==) on type t -> t -> Bool is available.

Aside: We may associate more than one method per type class.

There are a number of pre-defined type class instances such as Eq Int and so forth.

We can extend the set of types for which Eq is defined.

data WeekDay = Mo
             | Tue
             | Wed
             | Thur
             | Friday
             | Sat
             | Sun

eqWD Mo Mo         = True
eqWD Tue Tue       = True
eqWD Wed Wed       = True
eqWD Thur Thur     = True
eqWD Friday Friday = True
eqWD Sat Sat       = True
eqWD Sun Sun       = True
eqWD _ _           = False

instance Eq WeekDay where
   (==) = eqWD

Hence, the following application of member is possible.

testMember = member Mo (Cons Tue (Cons Mo Null))

We can define complex type (class) relations.

instance Eq a => Eq (List a) where
   Null == Null               = True
   (Cons x xs) == (Cons y ys) = x == y && xs == ys
   _ == _                     = False

The above defines equality for lists assuming we provide for equality among the elements.

Type-directed dictionary-translation

The (static) typing of programs is explained in terms of a variant of the Hindley/Milner system where we keep track of type class constraints resulting from the program text.

Recall

member x Null = False
member x (Cons y ys)
    | x == y    = True
    | otherwise = member x ys

From the program text we derive that the first argument x is of type a and the second parameter is of type List a and therefore y is of type a. The call x == y implies the type class (constraint) Eq a. Hence, member has type Eq a => a -> List a -> Bool where a is universally quantified.

Let's consider another (typing) example.

isNull xs = xs == Null

Null is of type List a. Hence, the call xs == Null implies the type class constraint Eq (List a). In Haskell, we try to reduce type class constraints as much as possible based on the given instances. From above, we find

instance Eq a => Eq (List a)

Therefore, Eq (List a) is reduced to Eq a. Recall that the instance declaration represents a recipe how to build on instance of Eq on type List a provided we are given an instance on type a. Hence, isNull has type Eq a => List a -> Bool where a is universally quantified.

The compiler exploits the typing information and instruments the program code with calls to the expected (type-specific) instances of the overloaded methods. For each constraint Eq a we need to supply a dictionary value which represents an instance of (==) on type a -> a -> Bool. The process of compiling type class programs is called the dictionary-passing translation.

In Haskell, we represent the dictionary for Eq a as a data type. The translation of member is then as follows.

data DictEq a = DictEqVal (a->a->Bool)
unDict (DictEqVal f) = f

memberDict :: DictEq a -> a -> List a -> Bool
memberDict d x Null = False
memberDict (DictEqVal eq) x (Cons y ys)
    | eq x y    = True
    | otherwise = memberDict (DictEqVal eq) x ys

Short summary:

Think of a value of type DictEq a as the vtable
Called dictionaries in Haskell speak
The "dictionary-passing translation" inserts the appropriate dictionaries.
This is based on the typing derivation where we effectively turn type class constraints into additional arguments (dictionaries).

Let's consider the dictionary-passing translation of the other examples.

testMember = member Mo (Cons Tue (Cons Mo Null))

translates to

testMemberDict = memberDict dictEqWD Mo (Cons Tue (Cons Mo Null))

where

instance Eq WeekDay where  ...
instance Eq a => Eq (List a) where ...

translates to

dictEqWD :: DictEq WeekDay
dictEqWD = DictEqVal eqWD

dictEqList :: DictEq t -> DictEq (List t)
dictEqList (DictEqVal eq) =
   DictEqVal (\x -> \y ->
               case (x,y) of
                 (Null, Null) -> True
                 (Cons x xs, Cons y ys) ->
                            (eq x y) &&
                            (unDict (dictEqList (DictEqVal eq))) xs ys)
                 _ -> False

Coherence Issues

The meaning of type class programs is tied to the typing of programs. If possible we seek for a coherent translation scheme where different typings lead to the (semantically speaking) same translation. Unfortunately, coherence is lost in general. See the following example.

class ShowRead a where
    show :: a -> String
    read :: String -> a

Via show we convert a value into a string (think of "printf") whereas read performs the opposite transformation (think of "scanf").

The interplay of both methods leads to incoherence. Consider

readShow s = show (read s)

A string is transformed into a type specific format and then again transformed into a string. The issue is that the type specific format is not exactly specified. Function readShow has type

readShow :: ShowRead a => String -> String

Notice the type class constraint ShowRead a where the parameter a is not constrained by the function type. Hence, when translating readShow we can possibly use any ShowRead instance (there are prefined instances for Int, Float, ...). Hence, different typings lead to different semantic meanings. Hence, coherence is lost.

Unambiguous types to guarantee coherence

In Haskell, the problem is fixed by disallowing programs such as readShow based on an additional static type check. The type ShowRead a => String -> String is considered ambiguous because of the unconstrained a. Ambiguous programs are rejected. For unambiguous programs, we can guarantee that the dictionary-passing translation is coherent.

A consequence of rejecting ambiguous programs is the loss of principal types. We say a type is principal for a program if all other types can be derived (as instances) from this types. As we can see in the above example, the principal type is ambiguous. All unambiguous types are not principal.

A second look at overloading

In "A second look at overloading", Odersky, Wadler and Wehr suggest to restrict type classes to methods where only arguments may be overloaded. Technically, each method m belonging to type class TC a must be of the type a -> t for some type t. Notice that show satisfies this condition whereas read does not. Under this restriction, ambiguities cannot arise. That is, coherence and principal types hold in general for such restricted type class programs.

Extensions (Type class design space)

There exist many variants and extensions such as superclasses, multi-parameter type classes etc. Some extensions such as functional dependencies require extensions of the dictionary-passing translation (the target language needs to be enriched).

We briefly discuss superclasses.

class Eq a => Ord a

States that for each intance Ord t there must also an instance Eq t. In general, this requirement can be checked statically (based on the set of available instances).

In terms of the dictionary-passing translation, each dictionary for Ord also contains the respective dictionary for Eq.

data DictOrd a = DictOrdVal (DictEq a) (a->a->Bool)

Method overloading and interfaces in Go

Recall "Translating methods and interfaces" on the Go lecture notes.

The main difference to Haskell is that in Go we not only find a dictionary of method defintions but also the actual value that implements these definitions.

Aside. In Haskell, we can represent Go interfaces via existential data types and type classes.

Bounded polymorphism

In practice, a "generic" function works not necessarily for values of all types T. We often find "type bounds" (a.k.a. type constraints, ...).

Type bounds in C++ are implicit

#include <iostream>
#include <string>
using namespace std;


// Template specialization.
template<typename T>
string Show(T);

template<>
string Show(bool b) {
  return b ? "true" : "false";
}

template<>
string Show(int i) {
  return to_string(i);
}


// Swap again.
// Point to note.
// We're using an instance of Show on type T but this bound on T is not captured anywhere.
template<typename T>
void swapAndShow(T &x, T &y) {
  T tmp;

  cout << "\n before: " << Show<T>(x) << " " << Show<T>(y);
  tmp = x;
  x = y;
  y = tmp;
  cout << "\n after: " << Show<T>(x) << " " << Show<T>(y);
}


int main() {
  cout << Show<bool>(true);

  int x = 1; int y = 2;
  swapAndShow<int>(x,y);

  {
  short int x = 1; short int y = 2;
  // Geht nicht weil keine "short int" Instanz.
  //  swapAndShow<short int>(x,y);

  // Geht weil kein l-value.
  // Beachte, wir verwenden Referenzuebergabe,
  // deshalb muss Argument "lokalisierbar", ein l-value, sein.
  //  swapAndShow<int>((int)x,(int)y);
  }

}

Explicit type bounds in Go with Generics


package main

import "strconv"
import "fmt"

type Show interface {
    show() string
}


type INT int

func (x INT) show() string {
    return strconv.Itoa((int)(x))
}

type BOOL bool

func (x BOOL) show() string {
    return strconv.FormatBool((bool)(x))
}


func swapAndShow[T Show](x *T, y *T)  {

    s1 := "\n before " + (*x).show() + " " + (*y).show()
    fmt.Printf("%s",s1)

    tmp := *x
    *x = *y
    *y = tmp

    s2 := "\n before " + (*x).show() + " " + (*y).show()
    fmt.Printf("%s",s2)

}


func main() {
 var b BOOL
 b = true
 fmt.Printf("%s", b.show())

 var x,y INT

 x = 1
 y = 2

 swapAndShow[INT](&x,&y)
}

Dependent types

So far, we have seen the following.

Terms that depend on terms.

By "terms" we refer to expressions/constructs found in some programming language. For example, consider the following Go function that takes another function as an argument.

func apply(i int, f func(int) int) int {
    return f(i)
    }

Types that depend on types.

For example, slices used in the function below. The type of a slice depends on the type of the underlying elements.

func mapInt(f func(int) int, xs []int) []int {
    ys := make([]int, len(xs))
    for i, e := range xs {
        ys[i] = f(e)
    }

    return ys
}

Further examples are collection types as found in Java. Take the Vec type (constructor/operator) which depends on the type of the underlying elements. For example, Vec<int> describes a vector of Integer values.

Terms that depend on types.

Consider

func f_int(x int) int {
   var y int
   y = x + 1
   return y
}

where + depends on the types assigned to the program variables. Hence, we find here Integer addition.

If we change the types, use Floats instead of Integer, the meaing of + changes.

func f_float(x float32) float32 {
   var y float32
   y = x + 1
   return y
}

In case terms depend on types, we usually find a form of polymorphism. In the above, we find overloading (a special form of ad-hoc polymorphism).

Let's consider parametric polymorphism. This is not supported by Go (yet) but let's assume Go supports type abstraction. By type abstraction we mean that we can abstract over type parameters (as done in Java with generics).

Here is a recast of the mapInt example.

func map<A,B>(f func(A) B, xs []A) []B {
    ys := make([]<B>, len(xs))
    for i, e := range xs {
        ys[i] = f(e)
    }

    return ys
}

This is yet another example for terms depending on types.

There's a fourth dependency: Types that depend on terms.

Dependent types - Types that depend on terms

Here's an example using Go notation.

func concat<N,M>(xs []int<N>, ys []int<M>) []int<N+M> {
    zs := make([]int, len(xs)+len(ys))
    var i int
    for i = 0; i < len(xs); i++ {
        zs[i] = xs[i]
    }
    for i = len(xs); i < len(xs)+len(ys); i++ {
        zs[i] = ys[i-len(xs)]
    }

    return zs
}

We find value parameters N and M. The type []int<N> describes a slice of Integer elements of length N. This is an example of a type depending on a term.

Function concat appends two slices. Hence, the length of the resulting slice is the sum of the length of the two input slices. This is expressed via the return type []int<N+M>.

The above example shows that

via dependent types we can capture non-trivial program properties
type checking with dependent types becomes more involved because we need to carry out certain computations already at compile-time (when type checking the program).

Type checking for dependent types is undecidable in general. Hence, dependently typed languages such as Agda and Idris require the user to supply proofs for dependent type properties.

Note. The Halting problem is undecidable but for a specific function the user can verify (by providing a proof) that the function terminates.

Dependent types in Haskell

In languages with parametric polymorphism we can mimic dependent types by encoding values via types. The general idea is to introduce phantom types. These are types where some of the type parameters are not connected to any program terms. We will see such an example shortly.

For concreteness, we consider a simulation of dependent types in Haskell. Haskell is a prime example of a language with "rich types" where we can express many interesting program properties via types. Haskell has been the inspiration of many other languages such as Scala and Rust to name a few only. The following example can be reformulated in these languages.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}

-- Simulating dependent types in Haskell.

-- Natural numbers.
-- data Nat = Zero | Succ Nat
data Zero = Zero
data Succ n = Succ n

-- Length-indexed lists.
data List a n where
    Nil :: List a Zero
    Cons :: a -> List a m -> List a (Succ m)

-- Haskell's "printf" via overloading.
instance Show a => Show (List a n) where
   show Nil = "[]"
   show (Cons x Nil) = "[" ++ show x ++ "]"
   show (Cons x xs) = "[" ++ show x ++ "," ++ tail (show xs)

-- List examples.
listNonEmpty1 = Cons False Nil
listNonEmpty2 = Cons True (Cons False Nil)
listEmpty = Nil

-- Safe operations on list.
headSafe :: List a (Succ n) -> a
headSafe (Cons x _) = x

tailSafe :: List a (Succ n) -> List a n
tailSafe (Cons _ xs) = xs

-- Reversing a list won't change its length.
reverseProp :: List a n -> List a n
reverseProp Nil = Nil
reverseProp (Cons x xs) = snoc (reverseProp xs) x

-- Helper snoc takes a list [x1,...,xn] and an element x
-- and yields the list [x1,...,xn,x].
snoc :: List a n -> a -> List a (Succ n)
snoc Nil x = Cons x Nil
snoc (Cons x xs) y = Cons x (snoc xs y)


-- Appending two lists of length l and m, yields a list of length l+m.
-- 1. We need to find a representation for the sum of l and m.
-- 2. The user needs to implement append as well as providing a proof that the resulting length is l+m.
-- 3. The type checker will verify that the property "l+m" is satisfied.
--
-- The property "l+m" needs to be represented at the level of types.
-- For this purpose, we introduce the following data type.
data Sum x y z where
  Base :: Sum Zero x x
       -- Fact:
       --  0 + x     = x
  Step :: Sum x y z -> Sum (Succ x) y (Succ z)
       -- Rule:
       -- If x + y = z
       -- then (x+1) + y = (z+1)
       --
       -- The above rule is formulated inductively.


-- Insight: Proofs are programs.
-- Consider the property that 1 + 2 = 3
-- where the below program represents a proof for this property.
onePlusTwoEqualsThree :: Sum (Succ Zero) (Succ (Succ Zero)) (Succ (Succ (Succ Zero)))
onePlusTwoEqualsThree = Step Base


-- Let's consider the append function.
-- As an additional (first) argument we find a proof for the to be verified property ("l+m").
-- We make use of the proof during the construction of the program.
-- The type checker ensures that the program satisfies the property.
appendProp :: Sum l m n -> List a l -> List a m -> List a n
appendProp Base Nil xs = xs
appendProp (Step p) (Cons x xs) ys = Cons x (appendProp p xs ys)


example = appendProp onePlusTwoEqualsThree listNonEmpty1 listNonEmpty2


-- We make use of some Haskell extension to let the compiler
-- infer the proof of the "l+m" property for us.

type family Plus x y
type instance Plus Zero x = x
type instance Plus (Succ x) y = Succ (Plus x y)

-- The proof for the propery "l+m" is now implicit.
-- The compiler will carry out the proof steps for us
-- and insert the proof into the program text.
appendProp2 :: List a l -> List a m -> List a (Plus l m)
appendProp2 Nil xs = xs
appendProp2 (Cons x xs) ys = Cons x (appendProp2 xs ys)

Dependent types in C++

// Simulating dependent types in C++11 with templates.

#include <iostream>
#include <string>
using namespace std;

// Natural numbers.
class Zero {};

template<typename N>
class Succ{
  public:
  Succ(N x) {}
};

enum ListKind {
  NilKind,
  ConsKind };

// Length indexed lists expressed as a template class.
// Each list carries its kind (nil or non-empty).
template<typename A, typename N>
class List {
   public:
   ListKind k;
};

// We distinguish between nil (empty) and non-empty list.
// Non-empty list are built via Cons and consist of a head and tail.
// The list [x1,...,xn] is represented as Cons x1 (... (Cons xn Nil) ...).
template<typename A>
class Nil : public List<A,Zero> {
  public:
  Nil() { this->k = NilKind; }
};

template<typename A, typename N>
class Cons : public List<A,Succ<N>> {
  public:
  A x;
  List<A,N>* xs;
  Cons(A _x, List<A,N>* _xs) {
    this->k = ConsKind;
    x = _x;
    xs = _xs;
  }
};

// Show functions.
// Specific definitions for subclasses and length-indexed lists.
string show(string s) {
  return s;
}

string show(bool b) {
  if(b) {
    return "true";
  }
  return "false";
}

template<typename A>
string show(Nil<A> ys) {
  return "[]";
}

template<typename A>
string show(Cons<A,Zero> ys) {
    return ("[" + show(ys.x) + "]");
}

template<typename A, typename N>
string show(Cons<A,Succ<N>> ys) {

  string s = show(ys.xs);

  return ("[" + show(ys.x) + "," + s.substr(1,s.length()-1));
}

template<typename A>
string show(List<A,Zero>* ys) {
  Nil<A>* zs = (Nil<A>*)ys;

  return show(*zs);
}

template<typename A, typename N>
string show(List<A,Succ<N>>* ys) {
  Cons<A,N>* zs = (Cons<A,N>*)ys;

  if(zs->xs->k == NilKind) {
    return ("[" + show(zs->x) + "]");
  }

  string s = show(zs->xs);
  return ("[" + show(zs->x) + "," + s.substr(1,s.length()-1));
}

// Safe list functions.

// Extracting the head requires a non-empty list.
template<typename A, typename N>
A headSafe(List<A,Succ<N>>* ys) {
    Cons<A,N>* zs = (Cons<A,N>*)ys;

    return zs->x;
}

// Extracting the tail requires a non-empty list.
template<typename A, typename N>
List<A,N>* tailSafe(List<A,Succ<N>>* ys) {
    Cons<A,N>* zs = (Cons<A,N>*)ys;

    return zs->xs;
}

// Snoc [x1,...,xn] x = Cons (x1 (... (Cons x Nil) ...))
// "Snoc" expressed via overloaded functions.
template<typename A>
List<A,Succ<Zero>>* Snoc(List<A,Zero>* ys, A y) {
  return (new Cons<A,Zero>(y,ys));
}

template<typename A, typename N>
List<A,Succ<Succ<N>>>* Snoc(List<A,Succ<N>>* ys, A y) {
   Cons<A,N>* zs = (Cons<A,N>*)ys;

   return (new Cons<A,Succ<N>>(zs->x,Snoc(zs->xs,y)));
}


// The "reverse" function where
// we guarantee that the length of the list remains the same.
template<typename A>
List<A,Zero>* reverseProp(List<A,Zero>* ys) {
  return ys;
}

template<typename A, typename N>
List<A,Succ<N>>* reverseProp(List<A,Succ<N>>* ys) {
    Cons<A,N>* zs = (Cons<A,N>*)ys;

    return Snoc(reverseProp(zs->xs),zs->x);
}

// Next, we consider appending two lists of length l and m.
// We (statically) guarantee that the length of the resulting list is the sum of l and m.

// We express X+Y=Z via a template class
// and partial template specialization.
template<typename X, typename Y, typename Z>
class Sum{};

template<typename X>
class Sum<Zero,X,X>{};

template<typename X, typename Y, typename Z>
class Sum<Succ<X>,Y,Succ<Z>>{
   public:
      Sum(Sum<X,Y,Z> _x) { p = _x; }
      Sum<X,Y,Z> p;
};

// We represent append as static member and
// use again partial template specialization to cover the various cases.
template<typename A, typename X, typename Y, typename Z>
class Append {
  public:
  static List<A,Z>* append(Sum<X,Y,Z>, List<A,X>*, List<A,Y>*);
};

template<typename A, typename X>
class Append<A,Zero,X,X> {
  public:
  static List<A,X>* append(Sum<Zero,X,X> p, List<A,Zero>* xs, List<A,X>* ys) {
    return ys;
  }
};

template<typename A, typename X, typename Y, typename Z>
class Append<A,Succ<X>,Y,Succ<Z>> {
  public:
  static List<A,Succ<Z>>* append(Sum<Succ<X>,Y,Succ<Z>> s, List<A,Succ<X>>* ys, List<A,Y>* zs) {
     Cons<A,X>* vs = (Cons<A,X>*)ys;

     return (new Cons<A,Y>(vs->x, Append<A,X,Y,Z>::append(s.p,vs->xs,zs)));
  }
};


// Examples.
int main() {

  // Lists of Booleans.
  {
  List<bool,Succ<Zero>>* l1 = new Cons<bool,Zero>(true,new Nil<bool>());
  List<bool,Succ<Succ<Zero>>>* l2 = new Cons<bool,Succ<Zero>>(false,l1);


  cout << "\n" << show(l1);

  cout << "\n" << show(l2);

  cout << "\n" << show(reverseProp(l2));

  // 1 + 1 = 2
  Sum<Succ<Zero>,Succ<Zero>,Succ<Succ<Zero>>> p
    = Sum<Succ<Zero>,Succ<Zero>,Succ<Succ<Zero>>>(Sum<Zero,Succ<Zero>,Succ<Zero>>());

  cout << "\n" << show(Append<bool,Succ<Zero>,Succ<Zero>,Succ<Succ<Zero>>>::append(p,l1,l1));

  }

  // Lists of strings.
  {
  auto l1 = Nil<string>();

  auto l2 = Cons<string,Zero>("a",new Nil<string>());
  List<string,Succ<Zero>>* l3 = &l2;
  List<string,Succ<Succ<Zero>>>* l4 = new Cons<string,Succ<Zero>>("b",l3);

  cout << "\n" << show(l1);

  cout << "\n" << show(l3);

  cout << "\n" << show(l4);
  }

}

Dependent types in Agda

data N : Set where
  zero : N
  succ : N -> N

add : N -> N -> N
add zero x = x
add (succ x) y = succ (add x y)

data List (A : Set) : (n : N) -> Set where
  Nil : List A zero
  Cons : {n : N} ->  A -> List A n -> List A (succ n)

head : forall {A n} -> List A (succ n) -> A
head (Cons x xs) = x

tail : forall {A n} -> List A (succ n) -> List A n
tail (Cons x xs) = xs

snoc : forall {A m} -> List A m -> A -> List A (succ m)
snoc Nil x = Cons x Nil
snoc (Cons x xs) y = Cons x (snoc xs y)

reverse : forall {A m} -> List A m -> List A m
reverse Nil = Nil
reverse (Cons x xs) = snoc (reverse xs) x

append : forall {A m n} -> List A m -> List A n -> List A (add m n)
append Nil xs = xs
append (Cons x xs) ys = Cons x (append xs ys)

Proofs are programs

We apply here a form of the "proofs-are-programs" principle.

Types are propositions.
Well-typed programs serve as proofs.

In our running example, we express properties about length-indexed lists via types. There are many more possible applications.

Propositional Logic

(Deduction)     G, t |- t


(Modus Ponens)  G |- t1 -> t2     G |- t1
                --------------------------
                G |- t2

t stands for a proposition, like "It rains today"
t1 -> t2 stands for implication, like "If it rains today then we need an umbrella"
Deduction: Make use of any of our assumptions
Modus Ponens: If in t1 -> t2 we can establish t1 then we can follow (deduce) t2
Does the following statement hold: (a->b)->((c->a)->(c->b))?

Proofs are lambda terms

If you look closely, the logical deduction rules almost match the typing rules for the simply-typed lambda calculus.
Lambda terms serve as proofs.
Let's prove (a->b)->((c->a)->(c->b))

We find that

{} |-  \x -> \y -> \z-> x (y z) : (a->b)->((c->a)->(c->b))

Informally,

x is of type a->b
y is of type c->a
z is of type c
Hence, y z is of type a
Hence, x (y z) is of type b
Hence, \x -> \y -> \z-> x (y z) has type (a->b)->((c->a)->(c->b))
We can view \x -> \y -> \z-> x (y z) as a proof for the proposition (a->b)->((c->a)->(c->b))

Curry-Howard Isomorphism

Curry and Howard discovered the connection between proofs in logic and lambda terms.

Types correspond to proposition
Lambda-terms/programs are compact representation of deduction style proofs.

Lots of cool applications. For example, simply state the type/propositions and automatically infer the program!

References

Robert Harper, Type systems for programming languages

Benjamin Pierce's book collection: