Lambda calculus
(Advanced Functional Programming)
Jeremy Yallop
Computer Laboratory
University of Cambridge
January 2017
1/ 64
Course outline
2/ 64
Books
OCaml from the very
beginning
John Whitington
Coherent Press (2013)
Real World OCaml
Yaron Minsky,
Anil Madhavapeddy &
Jason Hickey
O’Reilly Media (2013)
Types and Programming
Languages
Benjamin C. Pierce
MIT Press (2002)
3/ 64
Tooling
OPAM
OCaml package manager
IOCaml
Linux / OSX / VirtualBox
Fω
Fω interpreter
4/ 64
Philosophy and approach
▶ practical: with theory as necessary for understanding
▶ real-world: patterns and techniques from real applications
▶ reusable: general, broadly applicable techniques
▶ current: topics of ongoing research
▶ opinionated (but you don’t have to agree)
5/ 64
Philosophy and approach
▶ practical: with theory as necessary for understanding
▶ real-world: patterns and techniques from real applications
▶ reusable: general, broadly applicable techniques
▶ current: topics of ongoing research
▶ opinionated (but you don’t have to agree)
5/ 64
Mailing list
cl-acs-28@lists.cam.ac.uk
Announcements, questions and discussion. Feel free to post!
Have a question but feeling shy? Mail me directly and I’ll
anonymise and post your question:
jeremy.yallop@cl.cam.ac.uk
6/ 64
Exercises assessed and unassessed
Unassessed exercises
Useful preparation for assessed exercises; optional but
recommended. Hand in for feedback, discuss freely on mailing list.
Assessed exercises
Mon 30 Jan
↓
Mon 13 Feb
(∼30%)
Mon 20 Feb
↓
Mon 6 Mar
(∼35%)
Mon 13 Mar
↓
Tue 25 Apr
(∼35%)
7/ 64
Course structure
▶ Technical background
Lambda calculus; type inference
▶ Themes
Propositions as types; parametricity and abstraction
▶ (Fancy) types
Higher-rank and higher-kinded polymorphism; modules and
functors; generalised algebraic types; structured overloading
▶ Patterns and techniques
Monads, applicatives, arrows, etc.; datatype-generic
programming; staged programming
▶ Applications
(E.g.) a foreign function library
8/ 64
Motivation & background
9/ 64
System Fω
Function composition in OCaml:
fun f g x -> f (g x)
Function composition in System Fω:
Λα::∗.
Λβ::∗.
Λγ::∗.
λf:α → β.
λg:γ → α.
λx:γ.f (g x)
10/ 64
What’s the point of System Fω?
A framework for understanding language features and
programming patterns:
▶ the elaboration language for type inference
▶ the proof system for reasoning with propositional logic
▶ the background for parametricity properties
▶ the language underlying higher-order polymorphism in OCaml
▶ the elaboration language for modules
▶ the core calculus for GADTs
11/ 64
Roadmap
Fω
F
??��������
λ→
OO
12/ 64
Inference rules
premise 1
premise 2
. . .
premise N
rule name
conclusion
13/ 64
Inference rules
premise 1
premise 2
. . .
premise N
rule name
conclusion
all M are P
all S are M
modus barbara
all S are P
13/ 64
Inference rules
premise 1
premise 2
. . .
premise N
rule name
conclusion
all M are P
all S are M
modus barbara
all S are P
all programs are buggy
all functional programs are programs
modus barbara
all functional programs are buggy
13/ 64
Typing rules
Γ ⊢ M : A → B
Γ ⊢ N : A →-elim
Γ ⊢ M N : B
14/ 64
Terms, types, kinds
Kinds: K, K1, K2, . . .
K is a kind
Types: A, B, C, . . .
Γ ⊢ A :: K
Environments: Γ
Γ is an environment
Terms: L, M, N, . . .
Γ ⊢ M : A
15/ 64
λ→
(simply typed lambda calculus)
16/ 64
λ→ by example
In λ→:
λx:A.x
λf:B → C.
λg:A → B.
λx:A.f (g x)
In OCaml:
fun x -> x
fun f g x -> f (g x)
17/ 64
Kinds in λ→
∗-kind∗ is a kind
18/ 64
Kinding rules (type formation) in λ→
kind-B
Γ ⊢ B :: ∗
Γ ⊢ A :: ∗ Γ ⊢ B :: ∗
kind-→
Γ ⊢ A → B :: ∗
19/ 64
A kinding derivation
kind-B
Γ ⊢ B :: ∗ kind-BΓ ⊢ B :: ∗
kind-→
Γ ⊢ B → B :: ∗ kind-BΓ ⊢ B :: ∗
kind-→
Γ ⊢ (B → B) → B :: ∗
20/ 64
Environment formation rules
Γ-·· is an environment
Γ is an environment Γ ⊢ A :: ∗
Γ-:
Γ, x : A is an environment
21/ 64
Typing rules (term formation) in λ→
x : A ∈ Γ
tvar
Γ ⊢ x : A
Γ, x : A ⊢ M : B
→-intro
Γ ⊢ λx:A.M : A → B
Γ ⊢ M : A → B
Γ ⊢ N : A →-elim
Γ ⊢ M N : B
22/ 64
A typing derivation for the identity function
·, x : A ⊢ x : A
→-intro· ⊢ λx:A.x : A → A
23/ 64
Products by example
In λ→ with products:
λp:(A → B)× A.
f s t p (snd p)
λx:A.⟨x,x⟩
λf:A → C.
λg:B → C.
λp:A× B.
⟨f ( f s t p),
g (snd p)⟩
λp.A× B.⟨snd p, f s t p⟩
In OCaml:
fun (f,p) -> f p
fun x -> (x, x)
fun f g (x,y) -> (f x, g y)
fun (x,y) -> (y,x)
24/ 64
Kinding and typing rules for products
Γ ⊢ A :: ∗ Γ ⊢ B :: ∗
kind-×
Γ ⊢ A× B :: ∗
Γ ⊢ M : A
Γ ⊢ N : B ×-intro
Γ ⊢ ⟨M, N⟩ : A× B
Γ ⊢ M : A× B ×-elim-1
Γ ⊢ fst M : A
Γ ⊢ M : A× B ×-elim-2
Γ ⊢ snd M : B
25/ 64
Sums by example
In λ→ with sums:
λf:A → C.
λg:B → C.
λs:A+ B.
case s of
x.f x
| y.g y
λs:A+ B.
case s of
x. inr [B] x
| y. in l [A] y
In OCaml:
fun f g s ->
match s with
Inl x -> f x
| Inr y -> g y
function
Inl x -> Inr x
| Inr y -> Inl y
26/ 64
Kinding and typing rules for sums
Γ ⊢ A :: ∗ Γ ⊢ B :: ∗
kind-+
Γ ⊢ A+ B :: ∗
Γ ⊢ M : A
+-intro-1
Γ ⊢ inl [B] M : A+ B
Γ ⊢ N : B
+-intro-2
Γ ⊢ inr [A] N : A+ B
Γ ⊢ L : A+ B
Γ, x : A ⊢ M : C
Γ, y : B ⊢ N : C
+-elim
Γ ⊢ case L of x .M | y .N : C
27/ 64
System F
(polymorphic lambda calculus)
28/ 64
System F by example
Λα::∗.λx:α.x
Λα::∗.
Λβ::∗.
Λγ::∗.
λf:β → γ.
λg:α → β.
λx:α.f (g x)
Λα::∗.Λβ::∗.λp:(α → β)× α. f s t p (snd p)
29/ 64
New kinding rules for System F
Γ, α::K ⊢ A :: ∗
kind-∀
Γ ⊢ ∀α::K .A :: ∗
α::K ∈ Γ tyvar
Γ ⊢ α :: K
30/ 64
New environment rule for System F
Γ is an environment K is a kind
Γ-::
Γ, α::K is an environment
31/ 64
New typing rules for System F
Γ, α::K ⊢ M : A
∀-intro
Γ ⊢ Λα::K .M : ∀α::K .A
Γ ⊢ M : ∀α::K .A Γ ⊢ B :: K ∀-elim
Γ ⊢ M [B] : A[α::=B]
32/ 64