COMP3141 – Theory of Types
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Software System Design and Implementation
Theory of Types
Christine Rizkallah
UNSW Sydney
Term 2 2021
1
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Natural Deduction
Logic
We can specify a logical system as a deductive system by providing a set of rules and
axioms that describe how to prove properties about formulas involving various
connectives.
Each connective typically has introduction and elimination rules.
For example, to prove an implication A→ B holds, we must show that B holds
assuming A. This introduction rule is written as:
A, Γ ` B
Γ ` A→ B
→-I
derivability
(if the top, then the bottom)
entailment
(assuming the left, we can prove the right)
2
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Natural Deduction
Logic
We can specify a logical system as a deductive system by providing a set of rules and
axioms that describe how to prove properties about formulas involving various
connectives.
Each connective typically has introduction and elimination rules.
For example, to prove an implication A→ B holds, we must show that B holds
assuming A. This introduction rule is written as:
A, Γ ` B
Γ ` A→ B
→-I
derivability
(if the top, then the bottom)
entailment
(assuming the left, we can prove the right)
3
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
More rules
Implication also has an elimination rule, that is also called modus ponens:
Γ ` A→ B Γ ` A
Γ ` B
→-E
Conjunction (and) has an introduction rule that follows our intuition:
Γ ` A Γ ` B
Γ ` A ∧ B
∧-I
It has two elimination rules:
Γ ` A ∧ B
Γ ` A
∧-E1
Γ ` A ∧ B
Γ ` B
∧-E2
4
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
More rules
Disjunction (or) has two introduction rules:
Γ ` A
Γ ` A ∨ B
∨-I1
Γ ` B
Γ ` A ∨ B
∨-I2
Disjunction elimination is a little unusual:
Γ ` A ∨ B A, Γ ` P B, Γ ` P
Γ ` P
∨-E
The true literal, written >, has only an introduction:
Γ ` >
And false, written ⊥, has just elimination (ex falso quodlibet):
Γ ` ⊥
Γ ` P
5
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Example Proofs
Example
Prove:
A ∧ B → B ∧ A
A ∨ ⊥ → A
What would negation be equivalent to?
Typically we just define
¬A ≡ (A→ ⊥)
.
Example
Prove:
A→ (¬¬A)
(¬¬A)→ A We get stuck here!
6
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Example Proofs
Example
Prove:
A ∧ B → B ∧ A
A ∨ ⊥ → A
What would negation be equivalent to?
Typically we just define
¬A ≡ (A→ ⊥)
.
Example
Prove:
A→ (¬¬A)
(¬¬A)→ A We get stuck here!
7
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Example Proofs
Example
Prove:
A ∧ B → B ∧ A
A ∨ ⊥ → A
What would negation be equivalent to?
Typically we just define
¬A ≡ (A→ ⊥)
.
Example
Prove:
A→ (¬¬A)
(¬¬A)→ A We get stuck here!
8
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Example Proofs
Example
Prove:
A ∧ B → B ∧ A
A ∨ ⊥ → A
What would negation be equivalent to?
Typically we just define
¬A ≡ (A→ ⊥)
.
Example
Prove:
A→ (¬¬A)
(¬¬A)→ A We get stuck here!
9
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Example Proofs
Example
Prove:
A ∧ B → B ∧ A
A ∨ ⊥ → A
What would negation be equivalent to?
Typically we just define
¬A ≡ (A→ ⊥)
.
Example
Prove:
A→ (¬¬A)
(¬¬A)→ A
We get stuck here!
10
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Example Proofs
Example
Prove:
A ∧ B → B ∧ A
A ∨ ⊥ → A
What would negation be equivalent to?
Typically we just define
¬A ≡ (A→ ⊥)
.
Example
Prove:
A→ (¬¬A)
(¬¬A)→ A We get stuck here!
11
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Constructive Logic
The logic we have expressed so far does not admit the law of the excluded middle:
P ∨ ¬P
Or the equivalent double negation elimination:
(¬¬P)→ P
This is because it is a constructive logic that does not allow us to do proof by
contradiction.
12
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Boiling Haskell Down
The theoretical properties we will describe also apply to Haskell, but we need a smaller
language for demonstration purposes.
No user-defined types, just a small set of built-in types.
No polymorphism (type variables)
Just lambdas (λx .e) to define functions or bind variables.
This language is a very minimal functional language, called the simply typed lambda
calculus, originally due to Alonzo Church.
Our small set of built-in types are intended to be enough to express most of the data
types we would otherwise define.
We are going to use logical inference rules to specify how expressions are given types
(typing rules).
13
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Function Types
We create values of a function type A→ B using lambda expressions:
x :: A, Γ ` e :: B
Γ ` λx . e :: A→ B
The typing rule for function application is as follows:
Γ ` e1 :: A→ B Γ ` e2 :: A
Γ ` e1 e2 :: B
What other types would be needed?
14
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Composite Data Types
In addition to functions, most programming languages feature ways to compose types
together to produce new types, such as:
Tuples
Records
Structs
Classes
Unions
15
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Composite Data Types
In addition to functions, most programming languages feature ways to compose types
together to produce new types, such as:
Tuples
Records
Structs
Classes
Unions
16
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Composite Data Types
In addition to functions, most programming languages feature ways to compose types
together to produce new types, such as:
Tuples
Records
Structs
Classes
Unions
17
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Composite Data Types
In addition to functions, most programming languages feature ways to compose types
together to produce new types, such as:
Tuples
Records
Structs
Classes
Unions
18
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Combining values conjunctively
We want to store two things in one value.
(might want to use non-compact slides for this one)
Haskell Tuples
type Point = (Float, Float)
midpoint (x1,y1) (x2,y2)
= ((x1+x2)/2, (y1+y2)/2)
19
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Combining values conjunctively
We want to store two things in one value.
(might want to use non-compact slides for this one)
Haskell Tuples
type Point = (Float, Float)
midpoint (x1,y1) (x2,y2)
= ((x1+x2)/2, (y1+y2)/2)
Haskell Datatypes
data Point =
Pnt { x :: Float
, y :: Float
}
midpoint (Pnt x1 y1) (Pnt x2 y2)
= ((x1+x2)/2, (y1+y2)/2)
midpoint’ p1 p2 =
= ((x p1 + x p2) / 2,
(y p1 + y p2) / 2)
20
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Combining values conjunctively
We want to store two things in one value.
(might want to use non-compact slides for this one)
Haskell Tuples
type Point = (Float, Float)
midpoint (x1,y1) (x2,y2)
= ((x1+x2)/2, (y1+y2)/2)
Haskell Datatypes
data Point =
Pnt { x :: Float
, y :: Float
}
midpoint (Pnt x1 y1) (Pnt x2 y2)
= ((x1+x2)/2, (y1+y2)/2)
midpoint’ p1 p2 =
= ((x p1 + x p2) / 2,
(y p1 + y p2) / 2)
C Structs
typedef struct point {
float x;
float y;
} point;
point midPoint (point p1, point p2) {
point mid;
mid.x = (p1.x + p2.x) / 2.0;
mid.y = (p2.y + p2.y) / 2.0;
return mid;
}
21
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Combining values conjunctively
We want to store two things in one value.
(might want to use non-compact slides for this one)
Haskell Tuples
type Point = (Float, Float)
midpoint (x1,y1) (x2,y2)
= ((x1+x2)/2, (y1+y2)/2)
Haskell Datatypes
data Point =
Pnt { x :: Float
, y :: Float
}
midpoint (Pnt x1 y1) (Pnt x2 y2)
= ((x1+x2)/2, (y1+y2)/2)
midpoint’ p1 p2 =
= ((x p1 + x p2) / 2,
(y p1 + y p2) / 2)
C Structs
typedef struct point {
float x;
float y;
} point;
point midPoint (point p1, point p2) {
point mid;
mid.x = (p1.x + p2.x) / 2.0;
mid.y = (p2.y + p2.y) / 2.0;
return mid;
}
Java
class Point {
public float x;
public float y;
}
Point midPoint (Point p1, Point p2) {
Point mid = new Point();
mid.x = (p1.x + p2.x) / 2.0;
mid.y = (p2.y + p2.y) / 2.0;
return mid;
}
22
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Combining values conjunctively
We want to store two things in one value.
(might want to use non-compact slides for this one)
Haskell Tuples
type Point = (Float, Float)
midpoint (x1,y1) (x2,y2)
= ((x1+x2)/2, (y1+y2)/2)
Haskell Datatypes
data Point =
Pnt { x :: Float
, y :: Float
}
midpoint (Pnt x1 y1) (Pnt x2 y2)
= ((x1+x2)/2, (y1+y2)/2)
midpoint’ p1 p2 =
= ((x p1 + x p2) / 2,
(y p1 + y p2) / 2)
C Structs
typedef struct point {
float x;
float y;
} point;
point midPoint (point p1, point p2) {
point mid;
mid.x = (p1.x + p2.x) / 2.0;
mid.y = (p2.y + p2.y) / 2.0;
return mid;
}
Java
class Point {
public float x;
public float y;
}
Point midPoint (Point p1, Point p2) {
Point mid = new Point();
mid.x = (p1.x + p2.x) / 2.0;
mid.y = (p2.y + p2.y) / 2.0;
return mid;
}
“Better” Java
class Point {
private float x;
private float y;
public Point (float x, float y) {
this.x = x; this.y = y;
}
public float getX() {return this.x;}
public float getY() {return this.y;}
public float setX(float x) {this.x=x;}
public float setY(float y) {this.y=y;}
}
Point midPoint (Point p1, Point p2) {
return new Point((p1.getX() + p2.getX()) / 2.0,
(p2.getY() + p2.getY()) / 2.0);
}
23
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Product Types
For simply typed lambda calculus, we will accomplish this with tuples, also called
product types.
(A,B)
We won’t have type declarations, named fields or anything like that. More than two
values can be combined by nesting products, for example a three dimensional vector:
(Int, (Int, Int))
24
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Constructors and Eliminators
We can construct a product type the same as Haskell tuples:
Γ ` e1 :: A Γ ` e2 :: B
Γ ` (e1, e2) :: (A,B)
The only way to extract each component of the product is to use the fst and snd
eliminators:
Γ ` e :: (A,B)
Γ ` fst e :: A
Γ ` e :: (A,B)
Γ ` snd e :: B
25
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Unit Types
Currently, we have no way to express a type with just one value. This may seem
useless at first, but it becomes useful in combination with other types.
We’ll introduce the unit type from Haskell, written (), which has exactly one
inhabitant, also written ():
Γ ` () :: ()
26
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Disjunctive Composition
We can’t, with the types we have, express a type with exactly three values.
Example (Trivalued type)
data TrafficLight = Red | Amber | Green
In general we want to express data that can be one of multiple alternatives, that
contain different bits of data.
Example (More elaborate alternatives)
type Length = Int
type Angle = Int
data Shape = Rect Length Length
| Circle Length | Point
| Triangle Angle Length Length
This is awkward in many languages. In Java we’d have to use inheritance. In C we’d
have to use unions.
27
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Disjunctive Composition
We can’t, with the types we have, express a type with exactly three values.
Example (Trivalued type)
data TrafficLight = Red | Amber | Green
In general we want to express data that can be one of multiple alternatives, that
contain different bits of data.
Example (More elaborate alternatives)
type Length = Int
type Angle = Int
data Shape = Rect Length Length
| Circle Length | Point
| Triangle Angle Length Length
This is awkward in many languages. In Java we’d have to use inheritance. In C we’d
have to use unions.
28
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Sum Types
We’ll build in the Haskell Either type to express the possibility that data may be one
of two forms.
Either A B
These types are also called sum types.
Our TrafficLight type can be expressed (grotesquely) as a sum of units:
TrafficLight ‘ Either () (Either () ())
29
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Constructors and Eliminators for Sums
To make a value of type Either A B, we invoke one of the two constructors:
Γ ` e :: A
Γ ` Left e :: Either A B
Γ ` e :: B
Γ ` Right e :: Either A B
We can branch based on which alternative is used using pattern matching:
Γ ` e :: Either A B x :: A, Γ ` e1 :: P y :: B, Γ ` e2 :: P
Γ ` (case e of Left x → e1; Right y → e2) :: P
30
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Examples
Example (Traffic Lights)
Our traffic light type has three values as required:
TrafficLight ‘ Either () (Either () ())
Red ‘ Left ()
Amber ‘ Right (Left ())
Green ‘ Right (Right ())
31
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
The Empty Type
We add another type, called Void, that has no inhabitants. Because it is empty, there
is no way to construct it.
We do have a way to eliminate it, however:
Γ ` e :: Void
Γ ` absurd e :: ?
32
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
The Empty Type
We add another type, called Void, that has no inhabitants. Because it is empty, there
is no way to construct it.
We do have a way to eliminate it, however:
Γ ` e :: Void
Γ ` absurd e :: P
If I have a variable of the empty type in scope, we must be looking at an expression
that will never be evaluated. Therefore, we can assign any type we like to this
expression, because it will never be executed.
33
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Gathering Rules
Γ ` e :: Void
Γ ` absurd e :: P Γ ` () :: ()
Γ ` e :: A
Γ ` Left e :: Either A B
Γ ` e :: B
Γ ` Right e :: Either A B
Γ ` e :: Either A B x :: A, Γ ` e1 :: P y :: B, Γ ` e2 :: P
Γ ` (case e of Left x → e1; Right y → e2) :: P
Γ ` e1 :: A Γ ` e2 :: B
Γ ` (e1, e2) :: (A,B)
Γ ` e :: (A,B)
Γ ` fst e :: A
Γ ` e :: (A,B)
Γ ` snd e :: B
Γ ` e1 :: A→ B Γ ` e2 :: A
Γ ` e1 e2 :: B
x :: A, Γ ` e :: B
Γ ` λx . e :: A→ B
34
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Removing Terms. . .
Γ ` Void
Γ ` P Γ ` ()
Γ ` A
Γ ` Either A B
Γ ` B
Γ ` Either A B
Γ ` Either A B A, Γ ` P B, Γ ` P
Γ ` P
Γ ` A Γ ` B
Γ ` (A,B)
Γ ` (A,B)
Γ ` A
Γ ` (A,B)
Γ ` B
Γ ` A→ B Γ ` A
Γ ` B
A, Γ ` B
Γ ` A→ B
This looks exactly like constructive logic!
Constructing a program of a certain type, also creates a proof of a certain proposition.
35
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Removing Terms. . .
Γ ` Void
Γ ` P Γ ` ()
Γ ` A
Γ ` Either A B
Γ ` B
Γ ` Either A B
Γ ` Either A B A, Γ ` P B, Γ ` P
Γ ` P
Γ ` A Γ ` B
Γ ` (A,B)
Γ ` (A,B)
Γ ` A
Γ ` (A,B)
Γ ` B
Γ ` A→ B Γ ` A
Γ ` B
A, Γ ` B
Γ ` A→ B
This looks exactly like constructive logic!
Constructing a program of a certain type, also creates a proof of a certain proposition.
36
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Removing Terms. . .
Γ ` Void
Γ ` P Γ ` ()
Γ ` A
Γ ` Either A B
Γ ` B
Γ ` Either A B
Γ ` Either A B A, Γ ` P B, Γ ` P
Γ ` P
Γ ` A Γ ` B
Γ ` (A,B)
Γ ` (A,B)
Γ ` A
Γ ` (A,B)
Γ ` B
Γ ` A→ B Γ ` A
Γ ` B
A, Γ ` B
Γ ` A→ B
This looks exactly like constructive logic!
Constructing a program of a certain type, also creates a proof of a certain proposition.
37
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
The Curry-Howard Correspondence
This correspondence goes by many names, but is usually attributed to Haskell Curry
and William Howard.
It is a very deep result:
Programming Logic
Types Propositions
Programs Proofs
Evaluation Proof Simplification
It turns out, no matter what logic you want to define, there is always a corresponding
λ-calculus, and vice versa.
Typed λ-Calculus Constructive Logic
Continuations Classical Logic
Monads Modal Logic
Linear Types, Session Types Linear Logic
Region Types Separation Logic
38
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
The Curry-Howard Correspondence
This correspondence goes by many names, but is usually attributed to Haskell Curry
and William Howard.
It is a very deep result:
Programming Logic
Types Propositions
Programs Proofs
Evaluation Proof Simplification
It turns out, no matter what logic you want to define, there is always a corresponding
λ-calculus, and vice versa.
Typed λ-Calculus Constructive Logic
Continuations Classical Logic
Monads Modal Logic
Linear Types, Session Types Linear Logic
Region Types Separation Logic
39
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Examples
Example (Commutativity of Conjunction)
andComm :: (A,B)→ (B,A)
andComm p = (snd p, fst p)
This proves A ∧ B → B ∧ A.
Example (Transitivity of Implication)
transitive :: (A→ B)→ (B → C )→ (A→ C )
transitive f g x = g (f x)
Transitivity of implication is just function composition.
40
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Examples
Example (Commutativity of Conjunction)
andComm :: (A,B)→ (B,A)
andComm p = (snd p, fst p)
This proves A ∧ B → B ∧ A.
Example (Transitivity of Implication)
transitive :: (A→ B)→ (B → C )→ (A→ C )
transitive f g x = g (f x)
Transitivity of implication is just function composition.
41
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Examples
Example (Commutativity of Conjunction)
andComm :: (A,B)→ (B,A)
andComm p = (snd p, fst p)
This proves A ∧ B → B ∧ A.
Example (Transitivity of Implication)
transitive :: (A→ B)→ (B → C )→ (A→ C )
transitive f g x = g (f x)
Transitivity of implication is just function composition.
42
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Examples
Example (Commutativity of Conjunction)
andComm :: (A,B)→ (B,A)
andComm p = (snd p, fst p)
This proves A ∧ B → B ∧ A.
Example (Transitivity of Implication)
transitive :: (A→ B)→ (B → C )→ (A→ C )
transitive f g x = g (f x)
Transitivity of implication is just function composition.
43
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Translating
We can translate logical connectives to types and back:
Tuples Conjunction (∧)
Either Disjunction (∨)
Functions Implication
() True
Void False
We can also translate our equational reasoning on programs into proof simplification
on proofs!
44
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Proof Simplification
Assuming A ∧ B, we want to prove B ∧ A.
We have this unpleasant proof:
A ∧ B
B
A ∧ B
A
A ∧ B
A
A ∧ A
A
B ∧ A
45
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Proof Simplification
Translating to types, we get:
Assuming x :: (A,B), we want to construct (B,A).
x :: (A,B)
B
x :: (A,B)
A
x :: (A,B)
A
(A,A)
A
(B,A)
46
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Proof Simplification
Translating to types, we get:
Assuming x :: (A,B), we want to construct (B,A).
x :: (A,B)
snd x :: B
x :: (A,B)
A
x :: (A,B)
A
(A,A)
A
(B,A)
47
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Proof Simplification
Translating to types, we get:
Assuming x :: (A,B), we want to construct (B,A).
x :: (A,B)
snd x :: B
x :: (A,B)
fst x :: A
x :: (A,B)
fst x :: A
(A,A)
A
(B,A)
48
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Proof Simplification
Translating to types, we get:
Assuming x :: (A,B), we want to construct (B,A).
x :: (A,B)
snd x :: B
x :: (A,B)
fst x :: A
x :: (A,B)
fst x :: A
(fst x , fst x) :: (A,A)
A
(B,A)
49
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Proof Simplification
Translating to types, we get:
Assuming x :: (A,B), we want to construct (B,A).
x :: (A,B)
snd x :: B
x :: (A,B)
fst x :: A
x :: (A,B)
fst x :: A
(fst x , fst x) :: (A,A)
snd (fst x , fst x) :: A
(B,A)
50
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Proof Simplification
Translating to types, we get:
Assuming x :: (A,B), we want to construct (B,A).
x :: (A,B)
snd x :: B
x :: (A,B)
fst x :: A
x :: (A,B)
fst x :: A
(fst x , fst x) :: (A,A)
snd (fst x , fst x) :: A
(snd x , snd (fst x , fst x)) :: (B,A)
51
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Proof Simplification
Translating to types, we get:
Assuming x :: (A,B), we want to construct (B,A).
x :: (A,B)
snd x :: B
x :: (A,B)
fst x :: A
x :: (A,B)
fst x :: A
(fst x , fst x) :: (A,A)
snd (fst x , fst x) :: A
(snd x , snd (fst x , fst x)) :: (B,A)
We know that
(snd x , snd (fst x , fst x)) = (snd x , fst x)
Let’s apply this simplification to our proof!
52
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Proof Simplification
Assuming x :: (A,B), we want to construct (B,A).
x :: (A,B)
snd x :: B
x :: (A,B)
fst x :: A
(snd x , fst x) ::(B,A)
Back to logic:
A ∧ B
B
A ∧ B
A
B ∧ A
53
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Proof Simplification
Assuming x :: (A,B), we want to construct (B,A).
x :: (A,B)
snd x :: B
x :: (A,B)
fst x :: A
(snd x , fst x) ::(B,A)
Back to logic:
A ∧ B
B
A ∧ B
A
B ∧ A
54
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Applications
As mentioned before, in dependently typed languages such as Agda and Idris, the
distinction between value-level and type-level languages is removed, allowing us to
refer to our program in types (i.e. propositions) and then construct programs of those
types (i.e. proofs).
Generally, dependent types allow us to use rich types not just for programming, but
also for verification via the Curry-Howard correspondence.
55
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Caveats
All functions we define have to be total and terminating.
Otherwise we get an inconsistent logic that lets us prove false things:
proof 1 :: P = NP
proof 1 = proof 1
proof 2 :: P 6= NP
proof 2 = proof 2
Most common calculi correspond to constructive logic, not classical ones, so principles
like the law of excluded middle or double negation elimination do not hold:
¬¬P → P
56
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Semiring Structure
These types we have defined form an algebraic structure called a commutative
semiring.
Laws for Either and Void:
Associativity: Either (Either A B) C ‘ Either A (Either B C )
Identity: Either Void A ‘ A
Commutativity: Either A B ‘ Either B A
Laws for tuples and 1
Associativity: ((A,B),C ) ‘ (A, (B,C ))
Identity: ((),A) ‘ A
Commutativity: (A,B) ‘ (B,A)
Combining the two:
Distributivity: (A, Either B C ) ‘ Either (A,B) (A,C )
Absorption: (Void,A) ‘ Void
What does ‘ mean here? It’s more than logical equivalence.
57
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Semiring Structure
These types we have defined form an algebraic structure called a commutative
semiring.
Laws for Either and Void:
Associativity: Either (Either A B) C ‘ Either A (Either B C )
Identity: Either Void A ‘ A
Commutativity: Either A B ‘ Either B A
Laws for tuples and 1
Associativity: ((A,B),C ) ‘ (A, (B,C ))
Identity: ((),A) ‘ A
Commutativity: (A,B) ‘ (B,A)
Combining the two:
Distributivity: (A, Either B C ) ‘ Either (A,B) (A,C )
Absorption: (Void,A) ‘ Void
What does ‘ mean here? It’s more than logical equivalence.
58
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Semiring Structure
These types we have defined form an algebraic structure called a commutative
semiring.
Laws for Either and Void:
Associativity: Either (Either A B) C ‘ Either A (Either B C )
Identity: Either Void A ‘ A
Commutativity: Either A B ‘ Either B A
Laws for tuples and 1
Associativity: ((A,B),C ) ‘ (A, (B,C ))
Identity: ((),A) ‘ A
Commutativity: (A,B) ‘ (B,A)
Combining the two:
Distributivity: (A, Either B C ) ‘ Either (A,B) (A,C )
Absorption: (Void,A) ‘ Void
What does ‘ mean here? It’s more than logical equivalence.
59
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Semiring Structure
These types we have defined form an algebraic structure called a commutative
semiring.
Laws for Either and Void:
Associativity: Either (Either A B) C ‘ Either A (Either B C )
Identity: Either Void A ‘ A
Commutativity: Either A B ‘ Either B A
Laws for tuples and 1
Associativity: ((A,B),C ) ‘ (A, (B,C ))
Identity: ((),A) ‘ A
Commutativity: (A,B) ‘ (B,A)
Combining the two:
Distributivity: (A, Either B C ) ‘ Either (A,B) (A,C )
Absorption: (Void,A) ‘ Void
What does ‘ mean here? It’s more than logical equivalence.
60
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Semiring Structure
These types we have defined form an algebraic structure called a commutative
semiring.
Laws for Either and Void:
Associativity: Either (Either A B) C ‘ Either A (Either B C )
Identity: Either Void A ‘ A
Commutativity: Either A B ‘ Either B A
Laws for tuples and 1
Associativity: ((A,B),C ) ‘ (A, (B,C ))
Identity: ((),A) ‘ A
Commutativity: (A,B) ‘ (B,A)
Combining the two:
Distributivity: (A, Either B C ) ‘ Either (A,B) (A,C )
Absorption: (Void,A) ‘ Void
What does ‘ mean here? It’s more than logical equivalence.
61
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Semiring Structure
These types we have defined form an algebraic structure called a commutative
semiring.
Laws for Either and Void:
Associativity: Either (Either A B) C ‘ Either A (Either B C )
Identity: Either Void A ‘ A
Commutativity: Either A B ‘ Either B A
Laws for tuples and 1
Associativity: ((A,B),C ) ‘ (A, (B,C ))
Identity: ((),A) ‘ A
Commutativity: (A,B) ‘ (B,A)
Combining the two:
Distributivity: (A, Either B C ) ‘ Either (A,B) (A,C )
Absorption: (Void,A) ‘ Void
What does ‘ mean here? It’s more than logical equivalence.
62
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Semiring Structure
These types we have defined form an algebraic structure called a commutative
semiring.
Laws for Either and Void:
Associativity: Either (Either A B) C ‘ Either A (Either B C )
Identity: Either Void A ‘ A
Commutativity: Either A B ‘ Either B A
Laws for tuples and 1
Associativity: ((A,B),C ) ‘ (A, (B,C ))
Identity: ((),A) ‘ A
Commutativity: (A,B) ‘ (B,A)
Combining the two:
Distributivity: (A, Either B C ) ‘ Either (A,B) (A,C )
Absorption: (Void,A) ‘ Void
What does ‘ mean here? It’s more than logical equivalence.
63
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Semiring Structure
These types we have defined form an algebraic structure called a commutative
semiring.
Laws for Either and Void:
Associativity: Either (Either A B) C ‘ Either A (Either B C )
Identity: Either Void A ‘ A
Commutativity: Either A B ‘ Either B A
Laws for tuples and 1
Associativity: ((A,B),C ) ‘ (A, (B,C ))
Identity: ((),A) ‘ A
Commutativity: (A,B) ‘ (B,A)
Combining the two:
Distributivity: (A, Either B C ) ‘ Either (A,B) (A,C )
Absorption: (Void,A) ‘ Void
What does ‘ mean here? It’s more than logical equivalence.
64
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Semiring Structure
These types we have defined form an algebraic structure called a commutative
semiring.
Laws for Either and Void:
Associativity: Either (Either A B) C ‘ Either A (Either B C )
Identity: Either Void A ‘ A
Commutativity: Either A B ‘ Either B A
Laws for tuples and 1
Associativity: ((A,B),C ) ‘ (A, (B,C ))
Identity: ((),A) ‘ A
Commutativity: (A,B) ‘ (B,A)
Combining the two:
Distributivity: (A, Either B C ) ‘ Either (A,B) (A,C )
Absorption: (Void,A) ‘ Void
What does ‘ mean here? It’s more than logical equivalence.
65
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Isomorphism
Two types A and B are isomorphic, written A ‘ B, if there exists a bijection between
them. This means that for each value in A we can find a unique value in B and vice
versa.
Example (Refactoring)
We can use this reasoning to simplify type definitions. For example:
data Switch = On Name Int
| Off Name
Can be simplified to the isomorphic (Name, Maybe Int).
Generic Programming
Representing data types generically as sums and products is the foundation for generic
programming libraries such as GHC generics. This allows us to define algorithms that
work on arbitrary data structures.
66
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Isomorphism
Two types A and B are isomorphic, written A ‘ B, if there exists a bijection between
them. This means that for each value in A we can find a unique value in B and vice
versa.
Example (Refactoring)
We can use this reasoning to simplify type definitions. For example:
data Switch = On Name Int
| Off Name
Can be simplified to the isomorphic (Name, Maybe Int).
Generic Programming
Representing data types generically as sums and products is the foundation for generic
programming libraries such as GHC generics. This allows us to define algorithms that
work on arbitrary data structures.
67
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Type Quantifiers
Consider the type of fst:
fst :: (a,b) -> a
This can be written more verbosely as:
fst :: forall a b. (a,b) -> a
Or, in a more mathematical notation:
fst :: ∀a b. (a, b)→ a
This kind of quantification over type variables is called parametric polymorphism or
just polymorphism for short.
(It’s also called generics in some languages, but this terminology is bad)
What is the analogue of ∀ in logic? (via Curry-Howard)?
68
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Curry-Howard
The type quantifier ∀ corresponds to a universal quantifier ∀, but it is not the same as
the ∀ from first-order logic. What’s the difference?
69
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Curry-Howard
The type quantifier ∀ corresponds to a universal quantifier ∀, but it is not the same as
the ∀ from first-order logic. What’s the difference?
First-order logic quantifiers range over a set of individuals or values, for example the
natural numbers:
∀x . x + 1 > x
These quantifiers range over propositions (types) themselves. It is analogous to
second-order logic, not first-order:
∀A. ∀B. A ∧ B → B ∧ A
∀A. ∀B. (A,B)→ (B,A)
The first-order quantifier has a type-theoretic analogue too (type indices), but this is
not nearly as common as polymorphism.
70
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Generality
If we need a function of type Int→ Int, a polymorphic function of type ∀a. a→ a
will do just fine, we can just instantiate the type variable to Int. But the reverse is not
true. This gives rise to an ordering.
Generality
A type A is more general than a type B, often written A v B, if type variables in A
can be instantiated to give the type B.
Example (Functions)
Int→ Int w ∀z . z → z w ∀x y . x → y w ∀a. a
71
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Generality
If we need a function of type Int→ Int, a polymorphic function of type ∀a. a→ a
will do just fine, we can just instantiate the type variable to Int. But the reverse is not
true. This gives rise to an ordering.
Generality
A type A is more general than a type B, often written A v B, if type variables in A
can be instantiated to give the type B.
Example (Functions)
Int→ Int w ∀z . z → z w ∀x y . x → y w ∀a. a
72
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Generality
If we need a function of type Int→ Int, a polymorphic function of type ∀a. a→ a
will do just fine, we can just instantiate the type variable to Int. But the reverse is not
true. This gives rise to an ordering.
Generality
A type A is more general than a type B, often written A v B, if type variables in A
can be instantiated to give the type B.
Example (Functions)
Int→ Int w ∀z . z → z w ∀x y . x → y w ∀a. a
73
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Constraining Implementations
How many possible total, terminating implementations are there of a function of the
following type?
Int→ Int
How about this type?
∀a. a→ a
Polymorphic type signatures constrain implementations.
74
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Constraining Implementations
How many possible total, terminating implementations are there of a function of the
following type?
Int→ Int
How about this type?
∀a. a→ a
Polymorphic type signatures constrain implementations.
75
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Constraining Implementations
How many possible total, terminating implementations are there of a function of the
following type?
Int→ Int
How about this type?
∀a. a→ a
Polymorphic type signatures constrain implementations.
76
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Parametricity
Definition
The principle of parametricity states that the result of polymorphic functions cannot
depend on values of an abstracted type.
More formally, suppose I have a polymorphic function g that is polymorphic on type a.
If run any arbitrary function f :: a→ a on all the a values in the input of g , that will
give the same results as running g first, then f on all the a values of the output.
Example
foo :: ∀a. [a]→ [a]
77
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Parametricity
Definition
The principle of parametricity states that the result of polymorphic functions cannot
depend on values of an abstracted type.
More formally, suppose I have a polymorphic function g that is polymorphic on type a.
If run any arbitrary function f :: a→ a on all the a values in the input of g , that will
give the same results as running g first, then f on all the a values of the output.
Example
foo :: ∀a. [a]→ [a]
We know that every element of the output occurs in the input.
The parametricity theorem we get is, for all f :
foo ◦ (map f ) = (map f ) ◦ foo
78
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
More Examples
head :: ∀a. [a]→ a
What’s the parametricity theorems?
79
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
More Examples
head :: ∀a. [a]→ a
What’s the parametricity theorems?
Example (Answer)
For any f :
f (head `) = head (map f `)
80
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
More Examples
(++) :: ∀a. [a]→ [a]→ [a]
What’s the parametricity theorem?
81
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
More Examples
(++) :: ∀a. [a]→ [a]→ [a]
What’s the parametricity theorem?
Example (Answer)
map f (a ++ b) = map f a ++ map f b
82
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
More Examples
concat :: ∀a. [[a]]→ [a]
What’s the parametricity theorem?
83
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
More Examples
concat :: ∀a. [[a]]→ [a]
What’s the parametricity theorem?
Example (Answer)
map f (concat ls) = concat (map (map f ) ls)
84
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Higher Order Functions
filter :: ∀a. (a→ Bool) → [a]→ [a]
What’s the parametricity theorem?
85
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Higher Order Functions
filter :: ∀a. (a→ Bool) → [a]→ [a]
What’s the parametricity theorem?
Example (Answer)
filter p (map f ls) = map f (filter (p ◦ f ) ls)
86
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Parametricity Theorems
Follow a similar structure. In fact it can be mechanically derived, using the relational
parametricity framework invented by John C. Reynolds, and popularised by Wadler in
the famous paper, “Theorems for Free!”1.
Upshot: We can ask lambdabot on the Haskell IRC channel for these theorems.
1
https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
87
https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
That’s it
We have now covered all the content in COMP3141. Thanks for sticking with the
course.
Functional Programming
Basics: Introduction to Haskell, Algebraic Data Types, Type Classes
Advanced Programming: Higher-Kinded Abstractions, Controlling Effects
Advanced Types: Rich Types and GADTs, Polymorphism, Parametricity,
Curry-Howard
Devising, Testing and Proving Program Properties
Equational Reasoning and Inductive Proofs,
Property-Based Testing using QuickCheck,
Program Specifications: Data Invariants, Data Refinement, and Functional
Correctness.
88
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Reminders
There is a quiz for this week, but no exercise (there’s still Assignment 2).
Curtis is giving a revision lecture this Thursday 3pm.
Next week’s lectures consist of an invited lecture and a second revision lecture
on Friday with Curtis.
Please come up with questions to ask Curtis for the revision lecture! It will be
over very quickly otherwise.
89
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Further Learning
UNSW courses:
COMP3161 — Concepts of Programming Languages
COMP4161 — Advanced Topics in Verification
COMP6721 — (In-)formal Methods
COMP3131 — Compilers
COMP4141 — Theory of Computation
COMP6752 — Modelling Concurrent Systems
COMP3151 — Foundations of Concurrency
COMP3153 — Algorithmic Verification
Online Learning
Oregon Programming Languages Summer School Lectures
(https://www.cs.uoregon.edu/research/summerschool/archives.html)
Videos are available from here! Also some on YouTube.
90
https://www.cs.uoregon.edu/research/summerschool/archives.html
Recap: Logic
Typed Lambda Calculus
Algebraic Type Isomorphism
Polymorphism and Parametricity
Wrap-up