程序代写代做代考 Lambda Calculus flex ocaml Lambda calculus – (Advanced Functional Programming)

Lambda calculus – (Advanced Functional Programming)

Roadmap

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

??��������

λ→

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

??��������

λω

OO

λ→

??�������

OO

Functional programming

// λC

/ / λP2

??��������

// λPω

OO

// λP

??�������

OO

Dependently-typed programming

36/ 37

Next time

Γ ⊢ M : ?

37/ 37