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