程序代写代做代考 ocaml Parametricity

Parametricity

Parametricity

Leo White

Jane Street

February 2017

1/ 70

Parametricity

▶ Polymorphism allows a single piece of code to be instantiated
with multiple types.

▶ Polymorphism is parametric when all of the instances behave
uniformly.

▶ Where abstraction hides details about an implementation
from the outside world, parametricity hides details about the
outside world from an implementation.

2/ 70

Parametricity in OCaml

3/ 70

Universal types in OCaml

4/ 70

Universal types in OCaml

(* ∀𝛼.𝛼 → 𝛼 *)
let f x = x

5/ 70

Universal types in OCaml

(* (∀𝛼.List𝛼 → 𝐼𝑛𝑡) → 𝐼𝑛𝑡 *)
let g h = h [1; 2; 3] + h [1.0; 2.0; 3.0]

Characters 27-30:
let g h = h [1; 2; 3] + h [1.0; 2.0; 3.0]

^^^
Error: This expression has type float

but an expression was expected of type int

6/ 70

Universal types in OCaml

Λ𝛼::*.𝜆f:𝛼 → Int.𝜆x:𝛼.𝜆y:𝛼.
plus (f x) (f y)

Λ𝛼::*.Λ𝛽::*.𝜆f:∀𝛾.𝛾 → Int.𝜆x:𝛼.𝜆y:𝛽.
plus (f [𝛼] x) (f [𝛽] y)

7/ 70

Universal types in OCaml

Λ𝛼::*.𝜆f:𝛼 → Int.𝜆x:𝛼.𝜆y:𝛼.
plus (f x) (f y)

Λ𝛼::*.Λ𝛽::*.𝜆f:∀𝛾.𝛾 → Int.𝜆x:𝛼.𝜆y:𝛽.
plus (f [𝛼] x) (f [𝛽] y)

7/ 70

Universal types in OCaml

fun f x y -> f x + f y

∀𝛼::*. (𝛼 → Int) → 𝛼 → 𝛼 → Int

∀𝛼::*.∀𝛽::*. (∀𝛾::*. 𝛾 → Int) → 𝛼 → 𝛽 → Int

8/ 70

Universal types in OCaml

(* ∀𝛼.List𝛼 → 𝐼𝑛𝑡 *)
type t = { h : ‘a. ‘a list -> int }

let len = {h = List.length}

(* (∀𝛼.List𝛼 → 𝐼𝑛𝑡) → 𝐼𝑛𝑡 *)
let g r = r.h [1; 2; 3] + r.h [1.0; 2.0; 3.0]

9/ 70

Higher-kinded polymorphism

f : ∀F::*→*.∀𝛼::*. F 𝛼 → (F 𝛼 → 𝛼) → 𝛼

x : List (Int × Int)

f x

10/ 70

Higher-kinded polymorphism

𝐹 𝛼 ∼ List(Int × Int)

𝐹 = List 𝛼 = Int × Int
𝐹 = Λ𝛽.List(𝛽 × 𝛽) 𝛼 = Int
𝐹 = Λ𝛽.List(Int × Int)

11/ 70

Lightweight higher-kinded polymorphism

A set F of functions such that:

∀𝐹, 𝐺 ∈ F. 𝐹 ≠ 𝐺 ⇒ ∀𝑡.𝐹(𝑡) ≠ 𝐺(𝑡)

12/ 70

Lightweight higher-kinded polymorphism

type ‘a t = (‘a * ‘a) list

13/ 70

Lightweight higher-kinded polymorphism

type lst = List
type opt = Option

type (‘a, ‘f) app =
| Lst : ‘a list -> (‘a, lst) app
| Opt : ‘a option -> (‘a, opt) app

(‘a, lst)app ≈ ‘a list

(‘a, opt)app ≈ ‘a option

14/ 70

Lightweight higher-kinded polymorphism

type ‘f map = {
map: ‘a ‘b. (‘a -> ‘b) ->

(‘a, ‘f) app -> (‘b, ‘f) app;
}

let f : ‘b map ->
(int, ‘b) app -> (string, ‘b) app =

fun m c ->
m.map

(fun x -> “Int: ” ^ (string_of_int x))
c

15/ 70

Lightweight higher-kinded polymorphism

let lmap : lst map =
{map = fun f (Lst l) -> Lst (List.map f l)}

let l = f lmap (Lst [1; 2; 3])

let omap : opt map =
{map = fun f (Opt o) -> Opt (Option.map f o)}

let o = f omap (Opt (Some 6))

16/ 70

Lightweight higher-kinded polymorphism

Generalised in the Higher library

17/ 70

Functors

18/ 70

Functors

module type Eq = sig
type t
val equal : t -> t -> bool

end

module type SetS = sig
type t
type elt
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val remove : elt -> t -> t
val to_list : t -> elt list

end

19/ 70

Functors

SetS with type elt = foo

expands to

sig
type t
type elt = foo
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val remove : elt -> t -> t
val to_list : t -> elt list

end

20/ 70

Functors

SetS with type elt := foo

expands to

sig
type t
val empty : t
val is_empty : t -> bool
val mem : foo -> t -> bool
val add : foo -> t -> t
val remove : foo -> t -> t
val to_list : t -> foo list

end

21/ 70

Functors
module Set (E : Eq)

: SetS with type elt := E.t = struct

type t = E.t list

let empty = []

let is_empty = function
| [] -> true
| _ -> false

let rec mem x = function
| [] -> false
| y :: rest ->

if (E.equal x y) then true
else mem x rest

let add x t =
if (mem x t) then t
else x :: t

22/ 70

Functors

let rec remove x = function
| [] -> []
| y :: rest ->

if (E.equal x y) then rest
else y :: (remove x rest)

let to_list t = t

end

23/ 70

Functors

module IntEq = struct
type t = int
let equal (x : int) (y : int) =

x = y
end

module IntSet = Set(IntEq)

24/ 70

Parametricity in System F𝜔

25/ 70

Universal types

SetImpl =
𝜆𝛾::*.𝜆𝛼::*.

𝛼
× (𝛼 → Bool)
× (𝛾 → 𝛼 → Bool)
× (𝛾 → 𝛼 → 𝛼)
× (𝛾 → 𝛼 → 𝛼)
× (𝛼 → List 𝛾)

empty = Λ𝛾::*.Λ𝛼::*.𝜆s:SetImpl 𝛾 𝛼.𝜋1 s
is_empty = Λ𝛾::*.Λ𝛼::*.𝜆s:SetImpl 𝛾 𝛼.𝜋2 s
mem = Λ𝛾::*.Λ𝛼::*.𝜆s:SetImpl 𝛾 𝛼.𝜋3 s
add = Λ𝛾::*.Λ𝛼::*.𝜆s:SetImpl 𝛾 𝛼.𝜋4 s
remove = Λ𝛾::*.Λ𝛼::*.𝜆s:SetImpl 𝛾 𝛼.𝜋5 s
to_list = Λ𝛾::*.Λ𝛼::*.𝜆s:SetImpl 𝛾 𝛼.𝜋6 s

26/ 70

Universal types

EqImpl =
𝜆𝛾::*.𝛾 → 𝛾 → Bool

equal = Λ𝛾::*.𝜆s:EqImpl 𝛾.s

27/ 70

Universal types

set_package =
Λ𝛾::*. 𝜆eq:EqImpl 𝛾.

pack List 𝛾,〈
nil [𝛾],
isempty [𝛾],
𝜆n:𝛾.fold [𝛾] [Bool]

(𝜆x:𝛾.𝜆y:Bool.or y (equal [𝛾] eq n x))
false,

cons [𝛾],
𝜆n:𝛾.fold [𝛾] [List 𝛾]

(𝜆x:𝛾.𝜆l:List 𝛾.
if (equal [𝛾] eq n x) [List 𝛾] l

(cons [𝛾] x l))
(nil [𝛾]),

𝜆l:List 𝛾.l 〉
as ∃𝛼::*.SetImpl 𝛾 𝛼

28/ 70

Universal types

Γ ⊢ 𝑀 ∶ ∀𝛼∶∶𝐾.𝐴 Γ ⊢ 𝐵 ∶∶ 𝐾 ∀-elimΓ ⊢ 𝑀 [𝐵] ∶ 𝐴[𝛼 ∶= 𝐵]

29/ 70

Relational parametricity

30/ 70

Relational parametricity

We can give precise descriptions of parametricity using relations
between types.

31/ 70

Relational parametricity

Given a type 𝑇 with free variables 𝛼, 𝛽1, … , 𝛽𝑛:

∀𝐵1. … ∀𝐵𝑛.∀𝑥 ∶ (∀𝛼.𝑇 [𝛼, 𝐵1, … , 𝐵𝑛]).
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.J𝑇 K[𝜌, =𝐵1 , … , =𝐵𝑛 ](𝑥[𝛾], 𝑥[𝛿])

32/ 70

Relational parametricity

Any value with a universal type must preserve all relations between
any two types that it can be instantiated with.

33/ 70

Theorems for free

34/ 70

Theorems for free

Parametricity applied to ∀𝛼.𝛼 → 𝛼:

∀𝑓 ∶ (∀𝛼.𝛼 → 𝛼).
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.

∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿.
𝜌(𝑢, 𝑣) ⇒ 𝜌(𝑓[𝛾] 𝑢, 𝑓[𝛿] 𝑣)

35/ 70

Theorems for free

Define a relation is𝑢 to represent being equal to a value 𝑢 ∶ 𝑇 :

is𝑢(𝑥 ∶ 𝑇 , 𝑦 ∶ 𝑇 ) = (𝑥 =𝑇 𝑢) ∧ (𝑦 =𝑇 𝑢)

36/ 70

Theorems for free

∀𝑓 ∶ (∀𝛼.𝛼 → 𝛼).
∀𝛾.∀𝑢 ∶ 𝛾.

is𝑢(𝑢, 𝑢) ⇒ is𝑢(𝑓[𝛾]𝑢, 𝑓[𝛾]𝑢)

37/ 70

Theorems for free

∀𝑓 ∶ (∀𝛼.𝛼 → 𝛼).
∀𝛾.∀𝑢 ∶ 𝛾.

𝑓[𝛾] 𝑢 =𝛾 𝑢

38/ 70

Theorems for free

Parametricity applied to ∀𝛼.List 𝛼 → List 𝛼:

∀𝑓 ∶ (∀𝛼.List 𝛼 → List 𝛼).
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.

∀𝑢 ∶ List 𝛾. ∀𝑣 ∶ List 𝛿.JList 𝛼K[𝜌](𝑢, 𝑣) ⇒ JList 𝛼K[𝜌](𝑓[𝛾] 𝑢, 𝑓[𝛿] 𝑣)

39/ 70

Theorems for free

The System F encoding for lists:
List 𝛼 = ∀𝛽. 𝛽 → (𝛼 → 𝛽 → 𝛽) → 𝛽

nil𝛼 = Λ𝛽. 𝜆n:𝛽. 𝜆c:𝛼 → 𝛽 → 𝛽. n

cons𝛼 = 𝜆x:𝛼. 𝜆xs:List 𝛼.
Λ𝛽. 𝜆n:𝛽. 𝜆c:𝛼 → 𝛽 → 𝛽.

c x (xs [𝛽] n c)

40/ 70

Theorems for free

The relational interpretation of the System F encoding for lists:

JList 𝛼K[𝜌] =
(𝑥 ∶ List𝐴, 𝑦 ∶ List𝐵).

∀𝛾. ∀𝛿. ∀𝜌′ ⊂ 𝛾 × 𝛿.
∀𝑛 ∶ 𝛾. ∀𝑚 ∶ 𝛿.
∀𝑐 ∶ 𝐴 → 𝛾 → 𝛾. ∀𝑑 ∶ 𝐵 → 𝛿 → 𝛿.

𝜌′(𝑛, 𝑚) ⇒
(∀𝑎 ∶ 𝐴. ∀𝑏 ∶ 𝐵. ∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿.

𝜌(𝑎, 𝑏) ⇒ 𝜌′(𝑢, 𝑣) ⇒ 𝜌′(𝑐 𝑎𝑢, 𝑑 𝑏𝑣)) ⇒
𝜌′(𝑥[𝛾]𝑛𝑐, 𝑦[𝛿]𝑚𝑑)

41/ 70

Theorems for free

If 𝑥 = 𝑛𝑖𝑙𝐴 and 𝑦 = 𝑛𝑖𝑙𝐵:

∀𝛾. ∀𝛿. ∀𝜌′ ⊂ 𝛾 × 𝛿.
∀𝑛 ∶ 𝛾. ∀𝑚 ∶ 𝛿.
∀𝑐 ∶ 𝐴 → 𝛾 → 𝛾. ∀𝑑 ∶ 𝐵 → 𝛿 → 𝛿.
∀𝑎 ∶ 𝐴.∀𝑢 ∶ 𝛾. ∀𝑏 ∶ 𝐵.∀𝑣 ∶ 𝛾.

𝜌′(𝑛, 𝑚) ⇒
(∀𝑎 ∶ 𝐴. ∀𝑏 ∶ 𝐵. ∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿.

𝜌(𝑎, 𝑏) ⇒ 𝜌′(𝑢, 𝑣) ⇒ 𝜌′(𝑐 𝑎𝑢, 𝑑 𝑏𝑣)) ⇒
𝜌′(𝑛𝑖𝑙𝐴[𝛾]𝑛𝑐, 𝑛𝑖𝑙𝐵[𝛿]𝑚𝑑)

42/ 70

Theorems for free

If 𝑥 = 𝑛𝑖𝑙𝐴 and 𝑦 = 𝑛𝑖𝑙𝐵:

∀𝛾. ∀𝛿. ∀𝜌′ ⊂ 𝛾 × 𝛿.
∀𝑛 ∶ 𝛾. ∀𝑚 ∶ 𝛿.
∀𝑐 ∶ 𝐴 → 𝛾 → 𝛾. ∀𝑑 ∶ 𝐵 → 𝛿 → 𝛿.
∀𝑎 ∶ 𝐴.∀𝑢 ∶ 𝛾. ∀𝑏 ∶ 𝐵.∀𝑣 ∶ 𝛾.

𝜌′(𝑛, 𝑚) ⇒
(∀𝑎 ∶ 𝐴. ∀𝑏 ∶ 𝐵. ∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿.

𝜌(𝑎, 𝑏) ⇒ 𝜌′(𝑢, 𝑣) ⇒ 𝜌′(𝑐 𝑎𝑢, 𝑑 𝑏𝑣)) ⇒
𝜌′(𝑛, 𝑚)

43/ 70

Theorems for free

If 𝑥 = 𝑛𝑖𝑙𝐴 and 𝑦 = 𝑛𝑖𝑙𝐵:

∀𝛾. ∀𝛿. ∀𝜌′ ⊂ 𝛾 × 𝛿.
∀𝑛 ∶ 𝛾. ∀𝑚 ∶ 𝛿.
∀𝑐 ∶ 𝐴 → 𝛾 → 𝛾. ∀𝑑 ∶ 𝐵 → 𝛿 → 𝛿.
∀𝑎 ∶ 𝐴.∀𝑢 ∶ 𝛾. ∀𝑏 ∶ 𝐵.∀𝑣 ∶ 𝛾.

𝜌′(𝑛, 𝑚) ⇒
(∀𝑎 ∶ 𝐴. ∀𝑏 ∶ 𝐵. ∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿.

𝜌(𝑎, 𝑏) ⇒ 𝜌′(𝑢, 𝑣) ⇒ 𝜌′(𝑐 𝑎𝑢, 𝑑 𝑏𝑣)) ⇒
𝜌′(𝑛, 𝑚)

44/ 70

Theorems for free

If 𝑥 = 𝑐𝑜𝑛𝑠𝐴 𝑖 𝑙 and 𝑦 = 𝑐𝑜𝑛𝑠𝐵 𝑗𝑘:

∀𝛾. ∀𝛿. ∀𝜌′ ⊂ 𝛾 × 𝛿.
∀𝑛 ∶ 𝛾. ∀𝑚 ∶ 𝛿.
∀𝑐 ∶ 𝐴 → 𝛾 → 𝛾. ∀𝑑 ∶ 𝐵 → 𝛿 → 𝛿.

𝜌′(𝑛, 𝑚) ⇒
(∀𝑎 ∶ 𝐴. ∀𝑏 ∶ 𝐵. ∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿.

𝜌(𝑎, 𝑏) ⇒ 𝜌′(𝑢, 𝑣) ⇒ 𝜌′(𝑐 𝑎𝑢, 𝑑 𝑏𝑣)) ⇒
𝜌′(𝑐𝑜𝑛𝑠𝐴[𝛾] 𝑖 𝑙𝑛𝑐, 𝑐𝑜𝑛𝑠𝐵[𝛿] 𝑗𝑘𝑚𝑑)

45/ 70

Theorems for free

If 𝑥 = 𝑐𝑜𝑛𝑠𝐴 𝑖 𝑙 and 𝑦 = 𝑐𝑜𝑛𝑠𝐵 𝑗𝑘:

∀𝛾. ∀𝛿. ∀𝜌′ ⊂ 𝛾 × 𝛿.
∀𝑛 ∶ 𝛾. ∀𝑚 ∶ 𝛿.
∀𝑐 ∶ 𝐴 → 𝛾 → 𝛾. ∀𝑑 ∶ 𝐵 → 𝛿 → 𝛿.

𝜌′(𝑛, 𝑚) ⇒
(∀𝑎 ∶ 𝐴. ∀𝑏 ∶ 𝐵. ∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿.

𝜌(𝑎, 𝑏) ⇒ 𝜌′(𝑢, 𝑣) ⇒ 𝜌′(𝑐 𝑎𝑢, 𝑑 𝑏𝑣)) ⇒
𝜌′(𝑐 𝑖 (𝑙[𝛾] 𝑛 𝑐), 𝑑 𝑗 (𝑘[𝛾] 𝑚 𝑑))

46/ 70

Theorems for free

If 𝑥 = 𝑐𝑜𝑛𝑠𝐴 𝑖 𝑙 and 𝑦 = 𝑐𝑜𝑛𝑠𝐵 𝑗𝑘:

∀𝛾. ∀𝛿. ∀𝜌′ ⊂ 𝛾 × 𝛿.
∀𝑛 ∶ 𝛾. ∀𝑚 ∶ 𝛿.
∀𝑐 ∶ 𝐴 → 𝛾 → 𝛾. ∀𝑑 ∶ 𝐵 → 𝛿 → 𝛿.

𝜌′(𝑛, 𝑚) ⇒
(∀𝑎 ∶ 𝐴. ∀𝑏 ∶ 𝐵. ∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿.

𝜌(𝑎, 𝑏) ⇒ 𝜌′(𝑢, 𝑣) ⇒ 𝜌′(𝑐 𝑎𝑢, 𝑑 𝑏𝑣)) ⇒
𝜌′(𝑐 𝑖 (𝑙[𝛾]𝑛𝑐), 𝑑 𝑗 (𝑘[𝛾]𝑚𝑑))

47/ 70

Theorems for free

If 𝑥 = 𝑐𝑜𝑛𝑠𝐴 𝑖 𝑙 and 𝑦 = 𝑐𝑜𝑛𝑠𝐵 𝑗𝑘:

∀𝛾. ∀𝛿. ∀𝜌′ ⊂ 𝛾 × 𝛿.
∀𝑛 ∶ 𝛾. ∀𝑚 ∶ 𝛿.
∀𝑐 ∶ 𝐴 → 𝛾 → 𝛾. ∀𝑑 ∶ 𝐵 → 𝛿 → 𝛿.

𝜌′(𝑛, 𝑚) ⇒
(∀𝑎 ∶ 𝐴. ∀𝑏 ∶ 𝐵. ∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿.

𝜌(𝑎, 𝑏) ⇒ 𝜌′(𝑢, 𝑣) ⇒ 𝜌′(𝑐 𝑎𝑢, 𝑑 𝑏𝑣)) ⇒
𝜌(𝑖, 𝑗) ∧ 𝜌′(𝑙[𝛾]𝑛𝑐, 𝑘[𝛾]𝑚𝑑)

48/ 70

Theorems for free

The relational interpretation of the System F encoding for lists:

JList 𝛼K[𝜌](𝑥 ∶ List 𝐴, 𝑦 ∶ List 𝐵) =
⎧{
⎨{⎩

𝜌(𝑖, 𝑗) ∧ JList 𝛼K[𝜌](𝑙, 𝑘), 𝑥 = 𝑐𝑜𝑛𝑠𝐴 𝑖 𝑙 ∧ 𝑦 = 𝑐𝑜𝑛𝑠𝐵 𝑗𝑘
𝑡𝑟𝑢𝑒, 𝑥 = 𝑛𝑖𝑙𝐴 ∧ 𝑦 = 𝑛𝑖𝑙𝐵
𝑓𝑎𝑙𝑠𝑒, 𝑜𝑡ℎ𝑒𝑟𝑤𝑖𝑠𝑒

49/ 70

Theorems for free

Define a relation ⟨𝑔⟩ to represent a function 𝑔 ∶ 𝐴 → 𝐵

⟨𝑔⟩(𝑥 ∶ 𝐴, 𝑦 ∶ 𝐵) = (𝑔 𝑥 =𝐵 𝑦)

50/ 70

Theorems for free

Apply the relational interpretation for lists to ⟨𝑔⟩:

JList 𝛼K[⟨𝑔⟩](𝑥 ∶ List 𝐴, 𝑦 ∶ List 𝐵) =
⎧{
⎨{⎩

𝑔 𝑖 =𝐵 𝑗 ∧ JList 𝛼K[⟨𝑔⟩](𝑙, 𝑘), 𝑥 = 𝑐𝑜𝑛𝑠𝐴 𝑖 𝑙 ∧ 𝑦 = 𝑐𝑜𝑛𝑠𝐵 𝑗𝑘
𝑡𝑟𝑢𝑒, 𝑥 = 𝑛𝑖𝑙𝐴 ∧ 𝑦 = 𝑛𝑖𝑙𝐵
𝑓𝑎𝑙𝑠𝑒, 𝑜𝑡ℎ𝑒𝑟𝑤𝑖𝑠𝑒

51/ 70

Theorems for free

Apply the relational interpretation for lists to ⟨𝑔⟩:

JList 𝛼K[⟨𝑔⟩](𝑥𝑠 ∶ List 𝐴, 𝑦𝑠 ∶ List 𝐵) =
map[𝐴][𝐵] 𝑔 𝑥𝑠 =List 𝐵 𝑦𝑠

52/ 70

Theorems for free

A free theorem for ∀𝛼.List 𝛼 → List 𝛼:

∀𝑓 ∶ (∀𝛼.List 𝛼 → List 𝛼).
∀𝛾. ∀𝛿. ∀𝑔 ∶ 𝛾 → 𝛿

∀𝑢 ∶ List 𝛾. ∀𝑣 ∶ List 𝛿.
map[𝛾][𝛿] 𝑔 (𝑓[𝛾] 𝑢) = 𝑓[𝛿] (map[𝛾][𝛿] 𝑔 𝑢)

53/ 70

Terms and conditions apply

54/ 70

Terms and conditions apply

let f (x : ‘a) : ‘a =
Printf.printf “Launch missiles\n”;
x

let f (x : ‘a) : ‘a = raise Exit

let rec f (x : ‘a) : ‘a = f x

55/ 70

Terms and conditions apply

Parametricity applied to ∀𝛼.𝛼 → 𝛼 → Bool:

∀𝑓 ∶ (∀𝛼.𝛼 → 𝛼 → Bool).
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.

∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿. ∀𝑢′ ∶ 𝛾. ∀𝑣′ ∶ 𝛿.
𝜌(𝑢, 𝑣) ⇒ 𝜌(𝑢′, 𝑣′) ⇒J𝐵𝑜𝑜𝑙K[𝜌](𝑓[𝛾] 𝑢 𝑢′, 𝑓[𝛿]𝑣𝑣′)

56/ 70

Terms and conditions apply

Parametricity applied to ∀𝛼.𝛼 → 𝛼 → Bool:

∀𝑓 ∶ (∀𝛼.𝛼 → 𝛼 → Bool).
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.

∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿. ∀𝑢′ ∶ 𝛾. ∀𝑣′ ∶ 𝛿.
𝜌(𝑢, 𝑣) ⇒ 𝜌(𝑢′, 𝑣′) ⇒

(𝑓[𝛾] 𝑢 𝑢′ =𝐵𝑜𝑜𝑙 𝑓[𝛿]𝑣𝑣′)

57/ 70

Terms and conditions apply

∀𝑓 ∶ (∀𝛼.𝛼 → 𝛼 → Bool).
∀𝛾. ∀𝛿.

∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿. ∀𝑢′ ∶ 𝛾. ∀𝑣′ ∶ 𝛿.
(𝑓[𝛾] 𝑢 𝑢′ =𝐵𝑜𝑜𝑙 𝑓[𝛿]𝑣𝑣′)

58/ 70

Terms and conditions apply

val (=) : ‘a -> ‘a -> bool

59/ 70

60/ 70

Parametricity in geometery and mechanics

▶ Relational parametricity gives a good account of invariance
under change.

▶ The use of invariance under change to derive useful
consequences is a technique much older than programming
languages.

▶ Stepping beyond OCaml and System F𝜔 we can apply
parametricity to other areas of mathematics.

61/ 70

Parametricity in geometery and mechanics

Consider representing points as pairs of real numbers:
type point = real * real

The meaning of these real numbers depends on their choice of
origin.

62/ 70

Parametricity in geometery and mechanics

We add a new kind 𝑇2 to represent origins:

𝑇2 is a kind

63/ 70

Parametricity in geometery and mechanics

We define type-level operations for 𝑇2 corresponding to those of
an abelian group:

Γ ⊫ 0 ∶∶ 𝑇2

Γ ⊫ 𝐴 ∶∶ 𝑇2 Γ ⊫ 𝐵 ∶∶ 𝑇2
Γ ⊫ 𝐴 + 𝐵 ∶∶ 𝑇2

etc.

64/ 70

Parametricity in geometery and mechanics

Now we can index the point type by its choice of origin:
type ‘t point

and define various vector operations on them:
val (+) : ‘t point -> ‘s point -> (‘t + ‘s) point
val (-) : ‘t point -> ‘s point -> (‘t – ‘s) point
val cross : 0 point -> 0 point -> real

65/ 70

Parametricity in geometery and mechanics

The following function gives the area of a triangle represented by
three points:

let area a b c =
(abs (cross (c – a) (b – a))) / 2

it has type:
val area : ‘t point -> ‘t point -> ‘t point -> real

66/ 70

Parametricity in geometery and mechanics

From relational parametricity, the type:
‘t point -> ‘t point -> ‘t point -> real

gives a free theorem that the area of the triangle is invariant under
translation.

67/ 70

Parametricity in geometery and mechanics

By further enriching our type system with kinds for other
mathematical objects, we can take this even further.

68/ 70

Parametricity in geometery and mechanics

The following equation is a Lagrangian function describing a
mechanical system containing two particals of mass 𝑚 connected
by a spring with spring constant 𝑘 and constrained to move in
one-dimension:

𝐿(𝑡, 𝑥1, 𝑥2, ̇𝑥1, ̇𝑥2) =
1
2𝑚( ̇𝑥1

2 + ̇𝑥22) −
1
2𝑘(𝑥1 − 𝑥2)

2

69/ 70

Parametricity in geometery and mechanics

It can be given a type like this:

∀𝑦 ∶ T(1).
𝐶∞(ℝ(1, 0) × ℝ(1, 𝑦) × ℝ(1, 𝑦) × ℝ(1, 0) × ℝ(1, 0), ℝ(1, 0))

▶ Using relational parametricity, we can derive as a free theorem
of this type that the system is invariant to spatial translation.

▶ By Noether’s theorem, this demonstrates that the system
conserves linear momentum.

70/ 70