程序代写代做代考 Lambda Calculus ocaml interpreter Lambda calculus

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

??��������

λ→

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