CS计算机代考程序代写 data structure Lambda Calculus compiler Java Haskell concurrency algorithm Agda Hive Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
1
Software System Design and Implementation
Theory of Types
Christine Rizkallah
UNSW Sydney Term 2 2021

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Natural Deduction
Logic
2
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.

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
entailment
(assuming the left, we can prove the right)
3
derivability
(if the top, then the bottom)

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
→-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
4

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
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
5

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Example
Prove:
A∧B→B∧A
Example Proofs
6

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Example
Prove:
A∧B→B∧A A∨⊥→A
Example Proofs
7

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Example Proofs
Example
Prove:
A∧B→B∧A A∨⊥→A
8
What would negation be equivalent to?

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
.
Example
Prove:
A → (¬¬A)
¬A ≡ (A → ⊥)
9

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

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

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

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:

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
Structs
Records

18
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:
Classes
Tuples
Unions
Structs
Records

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 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)
Haskell Tuples
type Point = (Float, Float)
midpoint (x1,y1) (x2,y2) = ((x1+x2)/2, (y1+y2)/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)
C Structs
Haskell Datatypes
data Point = typedef struct point {
float x; Haskell Tuples
Pnt { x :: Float , y :: Float
midpoint (Pnt x1 y1) (Pnt x2 y2) = ((x1+x2)/2, (y1+y2)/2)
float y;
type Point }= p(oFilnota;t, Float)
}
point midPoint (point p1, point p2) {
midpoint (x1p,oyi1n)t(mxi2d,;y2)
= ((x1+x2)/m2i,d.(xy1=+y(2p)1/.2x)+ p2.x) / 2.0;
mid.y = (p2.y + p2.y) / 2.0;
return mid; }
midpoint’ p1 p2 =
= ((x p1 + x p2) / 2, (y p1 + y p2) / 2)
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)
23
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);

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

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) Γ ⊢ e :: (A,B) Γ ⊢ fst e :: A Γ ⊢ 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
27

28
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 Wrap-up

29
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 () ())

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 Γ ⊢ 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
30

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Examples
Example (Traffic Lights)
31
Our traffic light type has three values as required:
TrafficLight
Red
Amber
Green
≃ Either () (Either () ())
≃ Left()
≃ Right (Left ()) ≃ Right (Right ())

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 Γ⊢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.
33

Recap: Logic
Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Γ⊢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
34

Recap: Logic
Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
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
35

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 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
39

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Examples
Example (Commutativity of Conjunction)
40
This proves A ∧ B → B ∧ A.
andComm :: (A, B) → (B, A) andComm p = (snd p, fst p)

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

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Translating
We can translate logical connectives to types and back:
Tuples
Either
Functions
() Void
Conjunction (∧) Disjunction (∨) Implication True
False
44
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 Wrap-up
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
45

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
Translating to types, we get:
Assuming x :: (A,B), we want to construct (B,A).
Proof Simplification
x :: (A,B) fst x ::A
x :: (A,B) fst x ::A
(A,A) A
x :: (A,B) snd x :: B
48
(B,A)

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

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) x :: (A,B) snd x :: B fst x :: A
(snd x, fst x) ::(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).
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
54

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

56
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:
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

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)

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

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

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

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

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)

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)

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

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

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

68
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)?

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?

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

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.

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 ⊑ B, if type variables in A can be instantiated to give the type B.
72

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

75
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
How about this type?
Int → Int
∀a. a → a
Constraining Implementations
How many possible total, terminating implementations are there of a function of the following type?

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

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
77
foo :: ∀a. [a] → [a]

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
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
78

79
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
head :: ∀a. [a] → a What’s the parametricity theorems?
More Examples

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
head :: ∀a. [a] → a What’s the parametricity theorems?
More Examples
Example (Answer)
For any f :
80
f (head l) = head (map f l)

81
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
(++) :: ∀a. [a] → [a] → [a] What’s the parametricity theorem?
More Examples

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
(++) :: ∀a. [a] → [a] → [a]
What’s the parametricity theorem?
More Examples
Example (Answer)
82
mapf (a++b)=mapf a++mapf b

83
Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
concat :: ∀a. [[a]] → [a] What’s the parametricity theorem?
More Examples

Recap: Logic Typed Lambda Calculus Algebraic Type Isomorphism Polymorphism and Parametricity Wrap-up
concat :: ∀a. [[a]] → [a]
What’s the parametricity theorem?
More Examples
Example (Answer)
84
map f (concat ls) = concat (map (map f ) ls)

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?

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)
86
filterp(mapf ls)=mapf (filter(p◦f)ls)

87
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.
1https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf

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

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

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

Related Posts