Lambda calculus – (Advanced Functional Programming)
Roadmap
Fω
F
??��������
λ→
OO
1/ 37
Last time
λ→ → λx:A.M M N
sums +
inl [B] M
inr [A] M
case L of x .M | y .N
products × ⟨M, N⟩ fst M
snd M
polymorphism ∀ Λα::K .M M [B]
2/ 37
This time
λ→ → λx:A.M M N
sums
products
polymorphism ∀ Λα::K .M M [B]
existentials ∃ pack B,M
as ∃α::K .A
open M as
α,x in N
type operators ⇒ λα::K .B A B
3/ 37
This time: building data
1 bool N
+ lists
non-regular types ≡
4/ 37
Existential types
5/ 37
What’s the point of existentials?
▶ ∀ and ∃ in logic are closely connected to polymorphism and
existentials in type theory
▶ As in logic, ∀ and ∃ for types are closely related to each other
▶ Module types can be viewed as a kind of existential type
▶ OCaml’s variant types now support existential variables
6/ 37
Existential intuition
Existentials
correspond to
abstract types
7/ 37
Kinding rules for existentials
Γ, α::K ⊢ A :: ∗
kind-∃
Γ ⊢ ∃α::K .A :: ∗
8/ 37
Typing rules for existentials
Γ ⊢ M : A[α::=B] Γ ⊢ ∃α::K .A :: ∗
∃-intro
Γ ⊢ pack B,M as ∃α::K .A : ∃α::K .A
Γ ⊢ M : ∃α::K .A
Γ, α :: K , x : A ⊢ M ′ : B
∃-elim
Γ ⊢ open M as α, x in M ′ : B
9/ 37
Unit in OCaml
type u = Unit
10/ 37
Encoding data types in System F: unit
The unit type has one inhabitant.
We can represent it as the type of the identity function.
Unit = ∀α::∗.α → α
The unit value is the single inhabitant:
Unit = Λα::∗.λa:α.a
We can package the type and value as an existential:
pack (∀α::∗.α → α,
Λα::∗.λa:α.a)
as ∃U :: ∗.u
We’ll write 1 for the unit type and ⟨⟩ for its inhabitant.
11/ 37
Booleans in OCaml
A boolean data type:
type bool = False | True
A destructor for bool:
val _if_ : bool -> ’a -> ’a -> ’a
l e t _if_ b _then_ _else_ =
match b with
False -> _else_
| True -> _then_
12/ 37
Encoding data types in System F: booleans
The boolean type has two inhabitants: false and true.
We can represent it using sums and unit.
Bool = 1 + 1
The constructors are represented as injections:
false = in l [1] ⟨⟩
true = inr [1] ⟨⟩
The destructor ( if) is implemented using case:
λb:Bool.
Λα::∗.
λr:α.
λs:α.case b of x.s | y.r
13/ 37
Encoding data types in System F: booleans
We can package the definition of booleans as an existential:
pack (1+1,
⟨ inr [1] ⟨⟩,
⟨ in l [1] ⟨⟩,
λb:Bool.
Λα::∗.
λr:α.
λs:α.
case b of x.s | y.r⟩⟩)
as ∃β::∗.
β ×
β ×
(β → ∀α::∗.α → α → α)
14/ 37
Natural numbers in OCaml
A nat data type
type nat =
Zero : nat
| Succ : nat -> nat
A destructor for nat:
val foldNat : nat -> ’a -> (’a -> ’a) -> ’a
l e t rec foldNat n z s =
match n with
Zero -> z
| Succ n -> s (foldNat n z s)
15/ 37
Encoding data types in System F: natural numbers
The type of natural numbers is inhabited by Z, SZ, SSZ, …
We can represent it using a polymorphic function of two
parameters:
N = ∀α::∗.α → (α → α) → α
The Z and S constructors are represented as functions:
z : N
z = Λα::∗.λz:α.λs:α → α.z
s : N → N
s = λn:∀α::∗.α → (α → α) → α.
Λα::∗.λz:α.λs:α → α.s (n [α] z s),
The foldN destructor allows us to analyse natural numbers:
foldN : N → ∀α::∗.α → (α → α) → α
foldN = λn:∀α::∗.α → (α → α) → α.n
16/ 37
Encoding data types: natural numbers (continued)
foldN : N → ∀α::∗.α → (α → α) → α
For example, we can use foldN to write a function to test for zero:
λn:N.foldN n [Bool] true (λb:Bool.false)
Or we could instantiate the type parameter with N and write an
addition function:
λm:N.λn:N.foldN m [N] n succ
17/ 37
Encoding data types: natural numbers (concluded)
Of course, we can package the definition of N as an existential:
pack (∀α::∗.α → (α → α) → α,
⟨Λα::∗.λz:α.λs:α → α.z,
⟨λn:∀α::∗.α → (α → α) → α.
Λα::∗.λz:α.λs:α → α.s (n [α] z s),
⟨λn:∀α::∗.α → (α → α) → α.n⟩⟩⟩)
as ∃N::∗.
N ×
(N → N) ×
(N → ∀α::∗.α → (α → α) → α)
18/ 37
System Fω
(polymorphism + type abstraction)
19/ 37
System Fω by example
A kind for binary type operators
∗ ⇒ ∗ ⇒ ∗
A binary type operator
λα::∗.λβ::∗.α+ β
A kind for higher-order type operators
(∗ ⇒ ∗) ⇒ ∗ ⇒ ∗
A higher-order type operator
λϕ::∗ ⇒ ∗.λα::∗.ϕ (ϕ α)
20/ 37
Kind rules for System Fω
K1 is a kind K2 is a kind ⇒-kind
K1 ⇒ K2 is a kind
21/ 37
Kinding rules for System Fω
Γ, α::K1 ⊢ A :: K2 ⇒-intro
Γ ⊢ λα::K1.A :: K1 ⇒ K2
Γ ⊢ A :: K1 ⇒ K2
Γ ⊢ B :: K1 ⇒-elim
Γ ⊢ A B :: K2
22/ 37
Sums in OCaml
type (’a, ’b) sum =
Inl : ’a -> (’a, ’b) sum
| Inr : ’b -> (’a, ’b) sum
val case :
(’a, ’b) sum -> (’a -> ’c) -> (’b -> ’c) -> ’c
l e t case s l r =
match s with
Inl x -> l x
| Inr y -> r y
23/ 37
Encoding data types in System Fω: sums
We can finally define sums within the language.
As for N sums are represented as a binary polymorphic function:
Sum = λα::∗.λβ::∗.∀γ::∗.(α → γ) → (β → γ) → γ
The inl and inr constructors are represented as functions:
in l = Λα::∗.Λβ::∗.λv:α.Λγ::∗.
λl:α → γ.λr:β → γ.l v
inr = Λα::∗.Λβ::∗.λv:β.Λγ::∗.
λl:α → γ.λr:β → γ.r v
The foldSum function behaves like case:
foldSum =
Λα::∗.Λβ::∗.λc:∀γ::∗.(α → γ) → (β → γ) → γ.c
24/ 37
Encoding data types: sums (continued)
Of course, we can package the definition of Sum as an existential:
pack λα::∗.λβ::∗.∀γ::∗.(α → γ) → (β → γ) → γ,
Λα::∗.Λβ::∗.λv:α.Λγ::∗.λl:α → γ.λr:β → γ.l v
Λα::∗.Λβ::∗.λv:β.Λγ::∗.λl:α → γ.λr:β → γ.r v
Λα::∗.Λβ::∗.λc:∀γ::∗.(α → γ) → (β → γ) → γ.c
as ∃ϕ::∗ ⇒ ∗ ⇒ ∗.
∀α::∗.∀β::∗.α → ϕ α β
× ∀α::∗.∀β::∗.β → ϕ α β
× ∀α::∗.∀β::∗.ϕ α β → ∀γ::∗.(α → γ) → (β → γ) → γ
(However, the pack notation becomes unwieldy as our definitions
grow.)
25/ 37
Lists in OCaml
A list data type:
type ’a list =
Nil : ’a list
| Cons : ’a * ’a list -> ’a list
A destructor for lists:
val foldList :
’a list -> ’b -> (’a -> ’b -> ’b) -> ’b
l e t rec foldList l n c =
match l with
Nil -> n
| Cons (x, xs) -> c x (foldList xs n c)
26/ 37
Encoding data types in System F: lists
We can define parameterised recursive types such as lists in
System Fω.
As for N lists are represented as a binary polymorphic function:
List = λα::∗.∀ϕ::∗ ⇒ ∗.ϕ α → (α → ϕ α → ϕ α) → ϕ α
The nil and cons constructors are represented as functions:
nil = Λα::∗.Λϕ::∗ ⇒ ∗.λn:ϕ α.λc:α → ϕ α → ϕ α.n
cons = Λα::∗.λx:α.λxs:List α.
Λϕ::∗ ⇒ ∗.λn:ϕ α.λc:α → ϕ α → ϕ α.
c x (xs [ϕ] n c)
The destructor corresponds to the foldList function:
foldList = Λα::∗.Λβ::∗.λc:α → β → β.λn:β.
λl:List α.l [λγ::∗.β] n c
27/ 37
Encoding data types: lists (continued)
We defined add for N, and we can define append for lists:
append = Λα::∗.
λl:List α.λr:List α.
foldList [α] [List α]
l r (cons [α])
28/ 37
Nested types in OCaml
A regular type:
type ’a tree =
Empty : ’a tree
| Tree : ’a tree * ’a * ’a tree -> ’a tree
A non-regular type:
type ’a perfect =
ZeroP : ’a -> ’a perfect
| SuccP : (’a * ’a) perfect -> ’a perfect
29/ 37
Encoding data types in System Fω: nested types
We can represent non-regular types like perfect in System Fω:
Perfect = λα::∗.∀ϕ::∗ ⇒ ∗.
(∀α::∗.α → ϕ α) →
(∀α::∗.ϕ (α× α) → ϕ α) →
ϕ α
This time the arguments to zeroP and succP are themselves
polymorphic:
zeroP = Λα::∗.λx:α.Λϕ::∗ ⇒ ∗.
λz:∀α::∗.α → ϕ α.λs:∀α::∗.ϕ (α× α) → ϕ α.
z [α] x
succP = Λα::∗.λp:Perfect (α× α).Λϕ::∗ ⇒ ∗.
λz:∀α::∗.α → ϕ α.λs:∀β::∗.ϕ (β × β) → ϕ β.
s [α] (p [ϕ] z s)
30/ 37
Encoding data types in System Fω: Leibniz equality
Recall Leibniz’s equality:
consider objects equal if they behave identically in any context
In System Fω:
Eq = λα::∗.λβ::∗.∀ϕ::∗ ⇒ ∗.ϕ α → ϕ β
31/ 37
Encoding data types in System Fω: Leibniz equality
(continued)
Eq = λα::∗.λβ::∗.∀ϕ::∗ ⇒ ∗.ϕ α → ϕ β
Equality is reflexive (A ≡ A):
refl : ∀α::∗.Eql α α
refl = Λα::∗.Λϕ::∗ ⇒ ∗.λx:ϕ α.x
and symmetric (A ≡ B → B ≡ A):
symm : ∀α::∗.∀β::∗.Eql α β → Eql β α
symm = Λα::∗.Λβ::∗.
λe:(∀ϕ::∗ ⇒ ∗.ϕ α → ϕ β).e [λγ::∗.Eq γ α] (refl [α])
and transitive (A ≡ B ∧ B ≡ C → A ≡ C ):
trans : ∀α::∗.∀β::∗.∀γ::∗.Eql α β → Eql β γ → Eql α γ
trans = Λα::∗.Λβ::∗.Λγ::∗.
λab:Eq α β.λbc:Eq β γ.bc [Eq α] ab
32/ 37
Terms and types from types and terms
term parameters type parameters
building terms λx : A.M Λα::K .M
building types λα::K .A
33/ 37
Terms and types from types and terms
term parameters type parameters
building terms λx : A.M Λα::K .M
building types Πx : A.B λα::K .A
33/ 37
The roadmap again
Fω
F
??��������
λ→
OO
34/ 37
The lambda cube
Fω // λC
F
??��������
// λP2
??��������
λω //
OO
λPω
OO
λ→ //
??�������
OO
λP
??�������
OO
35/ 37
Programming on the left face of the cube
Fω
F
??��������
λω
OO
λ→
??�������
OO
Functional programming
// λC
/ / λP2
??��������
// λPω
OO
// λP
??�������
OO
Dependently-typed programming
36/ 37
Next time
Γ ⊢ M : ?
37/ 37