Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
1
Software System Design and Implementation
Theory of Types
Liam O’Connor
University of Edinburgh LFCS (and UNSW) Term 2 2020
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
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 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
entailment
(assuming the left, we can prove the right)
2
derivability
(if the top, then the bottom)
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
More rules
Implication also has an elimination rule, that is also called modus ponens:
Γ⊢A→B Γ⊢A
→-E Conjunction (and) has an introduction rule that follows our intuition:
Γ⊢B
Γ⊢A Γ⊢B
∧-I Γ⊢A∧B
It has two elimination rules:
Γ⊢A∧B Γ⊢A∧B Γ⊢A ∧-E1 Γ⊢B ∧-E2
3
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
More rules
Disjunction (or) has two introduction rules:
Γ⊢A Γ⊢B
Γ ⊢ A ∨ B ∨-I1 Γ ⊢ A ∨ B ∨-I2
Disjunction elimination is a little unusual:
Γ ⊢ A ∨ B A, Γ ⊢ P B, Γ ⊢ P
Γ⊢P
The true literal, written ⊤, has only an introduction:
∨-E
Γ⊢⊤
And false, written ⊥, has just elimination (ex falso quodlibet):
Γ⊢⊥ Γ⊢P
4
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Example Proofs
Example
Prove:
A∧B→B∧A A∨⊥→A
What would negation be equivalent to? Typically we just define
.
Example
Prove:
A → (¬¬A) (¬¬A) → A
We get stuck here!
¬A ≡ (A → ⊥)
5
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
6
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.
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
7
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).
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
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?
8
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
9
Composite Data Types
In addition to functions, most programming languages feature ways to compose types together to produce new types, such as:
Classes
Tuples
Unions
Structs
Records
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Combining values conjunctively
We want to store two things in one value.
(might want to use non-compact slides for this one)
10
typedef struct point {
Haskell Tuples
floatpyu;blic float x; private float x;
private float y; type Point }= p(oFilnota;t, Float)
C Structs
Haskell Datatypes
data Point = Java
floactlxa;ss Point { class Point {
P“nBtet{texr”::JaFvlaoat
, y :: Float }
public float y;
public Point (float x, float y) {
point}midPoint (point p1, point p2) { this.x = x; this.y = y;
}
returmnimdi.dy;= (p2.y + p2.y) / 2.0;
} = ((x p1 + x p2) / 2,
midpoint (Pnt x1 y1) (Pnt x2 y2) Point midPoint (Point p1, Point p2) {
midpoint (x1p,oyi1n)t(mxi2}d,;y2)
public float getX() {return this.x;}
= ((x1+x2)/2, (y1+y2)/2) = ((x1+x2)/m2i,d.(xy1=+y(2p)1/.2x)+ p2.x) / 2.0;
}
(y p1 + y p2) / 2)
return new Point((p1.getX() + p2.getX()) / 2.0,
Point mid = new Point();
public float getY() {return this.y;}
mid.ym=ipd(u.pbxl2i.=cyf(l+poa1pt.2xs.eyt+)X(pf/2l.o2ax.t)0x;)/ {2t.hi0s;.x=x;}
midpoint’ p1 p2 = public float setY(float y) {this.y=y;}
return mid;
Point midPoint (Point p1, Point p2) {
(p2.getY() + p2.getY()) / 2.0);
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
11
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))
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
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) Γ ⊢ e :: (A,B) Γ ⊢ fst e :: A Γ ⊢ snd e :: B
12
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
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 ():
Γ ⊢ () :: ()
13
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
14
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.
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
15
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 () ())
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Constructors and Eliminators for Sums
To make a value of type Either A B, we invoke one of the two constructors: Γ ⊢ e :: A Γ ⊢ e :: B
Γ ⊢ Left e :: Either A 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
16
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Example (Traffic Lights)
Examples
17
Our traffic light type has three values as required:
TrafficLight
Red
Amber
Green
≃ Either () (Either () ())
≃ Left()
≃ Right (Left ())
≃ Right (Right (Left ()))
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
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 Γ⊢absurde:: 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.
18
Recap: Logic
Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Γ⊢e ::Void Γ ⊢ absurd e :: P
Γ ⊢ e :: A
Γ ⊢ Left e :: Either A B
Γ ⊢ () :: ()
Γ ⊢ e :: B
Gathering Rules
Γ ⊢ 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 Γ⊢e::(A,B) Γ⊢e::(A,B) Γ ⊢ (e1,e2) :: (A,B) Γ ⊢ fst e :: A Γ ⊢ snd e :: B
Γ⊢e1 ::A→B Γ⊢e2 ::A x ::A,Γ⊢e ::B Γ⊢e1 e2 ::B Γ⊢λx.e::A→B
19
Recap: Logic
Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Removing Terms. . .
Γ ⊢ Void
Γ ⊢ P Γ ⊢ ()
Γ⊢A Γ⊢B
Γ ⊢ Either A B Γ ⊢ Either A B
Γ ⊢ Either A B Γ ⊢ A Γ ⊢ B
Γ ⊢ (A,B)
Γ ⊢ A → B
A,Γ ⊢ P Γ⊢P
Γ ⊢ (A,B) Γ ⊢ A
B,Γ ⊢ P
Γ ⊢ (A,B)
Γ ⊢ B A, Γ ⊢ B
Γ ⊢ A
Γ⊢B Γ⊢A→B
This looks exactly like constructive logic!
20 If we can construct a program of a certain type, we have also created a proof of a
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
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 Programs Evaluation
Propositions Proofs
Proof Simplification
It turns out, no matter what logic you want to define, there is always a corresponding λ-calculus, and vice versa.
Typed λ-Calculus Continuations Monads
Linear Types, Session Types Region Types
Constructive Logic Classical Logic Modal Logic Linear Logic Separation Logic
21
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
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.
22
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Translating
We can translate logical connectives to types and back:
Tuples
Either
Functions
() Void
Conjunction (∧) Disjunction (∨) Implication True
False
23
We can also translate our equational reasoning on programs into proof simplification on proofs!
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Proof Simplification
Assuming A∧B, we want to prove B ∧A. We have this unpleasant proof:
A∧B A∧B AA
A∧B A∧A BA
B∧A
24
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Proof Simplification
Translating to types, we get:
Assuming x :: (A,B), we want to construct (B,A).
x :: (A,B) x :: (A,B) fst x ::A fst x ::A
x :: (A,B) (fst x,fst x) :: (A,A) snd x :: B snd (fst x,fst x) :: A
(snd x, snd (fst x, fst x)) :: (B, A)
25
We know that
Lets apply this simplification to our proof!
(snd x, snd (fst x, fst x)) = (snd x, fst x)
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Proof Simplification
Assuming x :: (A,B), we want to construct (B,A).
Back to logic:
x :: (A,B) x :: (A,B) snd x :: B fst x :: A
(snd x, fst x) ::(B, A)
A∧B A∧B BA
B∧A
26
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
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).
Peano Arithmetic
If there’s time, Liam will demo how to prove some basic facts of natural numbers in Agda, a dependently typed language.
Generally, dependent types allow us to use rich types not just for programming, but also for verification via the Curry-Howard correspondence.
27
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
28
Caveats
All functions we define have to be total and terminating.
Otherwise we get an inconsistent logic that lets us prove false things:
proof1 ::P=NP proof 1 = proof 1
proof2 :: P ̸= 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
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
29
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.
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
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.
30
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
31
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)?
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
32
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.
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
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 ⊑ B, if type variables in A can be instantiated to give the type B.
Example (Functions)
Int→Int ⊒ ∀z.z→z ⊒ ∀xy.x→y ⊒ ∀a.a
33
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
34
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.
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Definition
Parametricity
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
35
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
head :: ∀a. [a] → a What’s the parametricity theorems?
More Examples
Example (Answer)
For any f :
36
f (head l) = head (map f l)
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
(++) :: ∀a. [a] → [a] → [a]
What’s the parametricity theorem?
More Examples
Example (Answer)
37
mapf (a++b)=mapf a++mapf b
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
concat :: ∀a. [[a]] → [a]
What’s the parametricity theorem?
More Examples
Example (Answer)
38
map f (concat ls) = concat (map (map f ) ls)
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
Higher Order Functions
filter::∀a.(a→Bool) →[a]→[a] What’s the parametricity theorem?
Example (Answer)
39
filterp(mapf ls)=mapf (filter(p◦f)ls)
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
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.
40
1https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
Recap: Logic
Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity
41
1
2 3
4
That’s the entirety of the assessable course content for COMP3141. There is a quiz for this week, but no exercise (there’s still Assignment 2)
Next week’s lectures consist of a extension lecture video on dependent type systems, and a revision lecture on Wednesday with Curtis..
Please come up with questions to ask Curtis for the revision lecture! It will be over very quickly otherwise.
Wrap-up