Last time: abstraction and parametricity
∃
∀
1/ 53
This time: GADTs
a ≡ b
2/ 53
What we gain
⇓ Γ ⊢:
Γ ⊢:
⇓
(Addtionally, some programs become faster!)
3/ 53
What we gain
⇓ Γ ⊢:
Γ ⊢:
⇓
(Addtionally, some programs become faster!)
3/ 53
What it costs
We’ll need to:
describe our data more precisely
strengthen the relationship between data and types
look at programs through a propositions-as-types lens
4/ 53
What we’ll write
Non-regularity in constructor return types
type _ t = T : t1 → t2 t
Locally abstract types:
let f : type a b. a t → b t = function . . .
let g (type a) (type b) (x : a t) : b t = . . .
5/ 53
Nested types
6/ 53
Unconstrained trees
T
T
T
E a E
b E
c E
type ’a tree =
Empty : ’a tree
| Tree : ’a tree * ’a * ’a tree → ’a tree
7/ 53
Term inference for unconstrained trees
val ? : ’a tree → int
val ? : ’a tree → ’a option
val ? : ’a tree → ’a tree
8/ 53
Unconstrained trees: depth
T
T
T
E a E
b E
c E
1 + max
(1 + max
(1 + max
0
0)
0)
0
let rec depth : ’a.’a tree → int =
function
Empty → 0
| Tree (l,_,r) → 1 + max (depth l) (depth r)
9/ 53
Unconstrained trees: top
T
T
T
E a E
b E
c E
Some c
let top : ’a.’a tree → ’a option =
function
Empty → None
| Tree (_,v,_) → Some v
10/ 53
Unconstrained trees: swivel
T
T
T
E a E
b E
c E
T
E c T
E b T
E a E
let rec swivel : ’a.’a tree → ’a tree =
function
Empty → Empty
| Tree (l,v,r) → Tree (swivel r, v, swivel l)
11/ 53
Perfect leaf trees via nesting
S
S
S
Z
a b c d e f g h
type ’a perfect =
ZeroP : ’a → ’a perfect
| SuccP : (’a * ’a) perfect → ’a perfect
12/ 53
Perfect (branch) trees via nesting
T
a
T
(b, c)
T
((d, e), (f, g))
E
type _ ntree =
EmptyN : ’a ntree
| TreeN : ’a * (’a * ’a) ntree → ’a ntree
13/ 53
Term inference for perfect nested trees
val ? : ’a ntree → int
val ? : ’a ntree → ’a option
val ? : ’a ntree → ’a ntree
14/ 53
Perfect trees: depth
T
a
T
(b, c)
T
((d, e), (f, g))
E
1 +
1 +
1 +
0
let rec depthN : ’a.’a ntree → int =
function
EmptyN → 0
| TreeN (_,t) → 1 + depthN t
15/ 53
Perfect trees: top
T
a
T
(b, c)
T
((d, e), (f, g))
E
Some a
let rec topN : ’a.’a ntree → ’a option =
function
EmptyN → None
| TreeN (v,_) → Some v
16/ 53
Perfect trees: swivel
T
a
T
(b, c)
T
((d, e), (f, g))
E
T
a
T
(c, b)
T
((g, f), (e, d))
E
let rec swiv : ’a.(’a→’a) → ’a ntree → ’a ntree =
fun f t → match t with
EmptyN → EmptyN
| TreeN (v,t) →
TreeN (f v,swiv (fun (x,y) → (f y, f x)) t)
let swivelN p = swiv id p
17/ 53
GADTs
18/ 53
Perfect trees, take two
T[3]
T[2]
T[1]
E d E
b T[1]
E e E
a T[2]
T[1]
E f E
c T[1]
E g E
type (’a, _) gtree =
EmptyG : (’a,z) gtree
| TreeG : (’a,’n) gtree * ’a * (’a,’n) gtree → (’a,’n s)
gtree
19/ 53
Natural numbers
type z = Z
type _ s = S : ’n → ’n s
# let zero = Z;;
val zero : z = Z
# let three = S (S (S Z));;
val three : z s s s = S (S (S Z))
20/ 53
Term inference for perfect trees (GADTs)
val ? : (’a,’n) gtree → ’n
val ? : (’a,’n s) gtree → ’a
val ? : (’a,’n) gtree → (’a,’n) gtree
21/ 53
Perfect trees (GADTs): depth
T[2]
T[1]
E d E
b T[1]
E e E
S (depth
S (depth
Z))
let rec depthG : type a n.(a, n) gtree → n =
function
EmptyG → Z
| TreeG (l,_,_) → S (depthG l)
22/ 53
Perfect trees (GADTs): depth
type (’a, _) gtree =
EmptyG : (’a,z) gtree
| TreeG : (’a,’n) gtree * ’a * (’a,’n) gtree → (’a,’n s)
gtree
let rec depthG : type a n.(a, n) gtree → n =
function
EmptyG → Z
| TreeG (l,_,_) → S (depthG l)
Type refinement
In the EmptyG branch: n≡ z
In the TreeG branch: n≡ m s (for some m)
l : (a, m)gtree
depthG l : m
Polymorphic recursion
The argument to the recursive call has size m (s.t. s m≡ n)
23/ 53
Perfect trees (GADTs): top
T[2]
T[1]
E b E
a T[1]
E c E
a
let topG : type a n.(a,n s) gtree → a =
function TreeG (_,v,_) → v
24/ 53
Perfect trees (GADTs): top
type (’a, _) gtree =
EmptyG : (’a,z) gtree
| TreeG : (’a,’n) gtree * ’a * (’a,’n) gtree → (’a,’n s)
gtree
let topG : type a n.(a,n s) gtree → a =
function TreeG (_,v,_) → v
Type refinement
In an EmptyG branch we would have: n s≡ z
— impossible!
25/ 53
Perfect trees (GADTs): swivel
T[2]
T[1]
E b E
a T[1]
E c E
T[2]
T[1]
E c E
a T[1]
E b E
let rec swivelG : type a n.(a,n) gtree → (a,n) gtree =
function
EmptyG → EmptyG
| TreeG (l,v,r) → TreeG (swivelG r, v, swivelG l)
26/ 53
Perfect trees (GADTs): swivel
type (’a, _) gtree =
EmptyG : (’a,z) gtree
| TreeG : (’a,’n) gtree * ’a * (’a,’n) gtree → (’a,’n s)
gtree
let rec swivelG : type a n.(a,n) gtree → (a,n) gtree =
function
EmptyG → EmptyG
| TreeG (l,v,r) → TreeG (swivelG r, v, swivelG l)
Type refinement
In the EmptyG branch: n≡ z
In the TreeG branch: n≡ m s (for some m)
l, r : (a, m)gtree
swivelG l : (a, m)gtree
Polymorphic recursion
The argument to the recursive call has size m (s.t. s m≡ n)
27/ 53
Zipping perfect trees
T[2]
T[1]
E b E
a T[1]
E c E
T[2]
T[1]
E e E
d T[1]
E f E
T[2]
T[1]
E (b,e) E
(a,d) T[1]
E (c,f) E
let rec zipTree :
type a b n.(a,n) gtree → (b,n) gtree →
(a * b,n) gtree =
fun x y → match x, y with
EmptyG , EmptyG → EmptyG
| TreeG (l,v,r), TreeG (m,w,s) →
TreeG (zipTree l m, (v,w), zipTree r s)
28/ 53
Zipping perfect trees
type (’a, _) gtree =
EmptyG : (’a,z) gtree
| TreeG : (’a,’n) gtree * ’a * (’a,’n) gtree → (’a,’n s)
gtree
let rec zipTree :
type a b n.(a,n) gtree → (b,n) gtree → (a * b,n)
gtree =
fun x y → match x, y with
EmptyG , EmptyG → EmptyG
| TreeG (l,v,r), TreeG (m,w,s) →
TreeG (zipTree l m, (v,w), zipTree r s)
Type refinement
In the EmptyG branch: n≡ z
In the TreeG branch: n≡ m s (for some m)
EmptyG, TreeG _ produces n≡ z and n≡ m s
— impossible!
29/ 53
Conversions between perfect tree representations
T[2]
T[1]
E b E
a T[1]
E c E
T
a
T
(b, c)
E
let rec nestify : type a n.(a,n) gtree → a ntree =
function
EmptyG → EmptyN
| TreeG (l, v, r) →
TreeN (v, nestify (zipTree l r))
30/ 53
Depth-annotated trees
T[2]
max(1,0)≡1
T[1]
max(0,0)≡0
E a E
b E
type (’a,_) dtree =
EmptyD : (’a,z) dtree
| TreeD : (’a,’m) dtree * ’a * (’a,’n) dtree * (’m,’n,’o) max
→ (’a,’o s) dtree
31/ 53
The untyped maximum function
val max : ’a → ’a → ’a
Parametricity: max is one of
fun x _ → x
fun _ y → y
32/ 53
A typed maximum function
val max : (’a,’b,’c) max → ’a → ’b → ’c
(max (a,b)≡ c) → a → b → c
33/ 53
A typed maximum function: a max predicate
type (_,_,_) max =
MaxEq : (’a,’a,’a) max
| MaxFlip : (’a,’b,’c) max → (’b,’a,’c) max
| MaxSuc : (’a,’b,’a) max → (’a s,’b,’a s) max
a≡ b → max(a,b)≡ a
max(a,b)≡ c → max(b,a)≡ c
max(a,b)≡ a → max(a+1,b)≡ a+1
34/ 53
A typed maximum function
type (_,_) eql = Refl : (’a,’a) eql
type (_,_,_) max =
MaxEq : (’a,’a,’a) max
| MaxFlip : (’a,’b,’c) max → (’b,’a,’c) max
| MaxSuc : (’a,’b,’a) max → (’a s,’b,’a s) max
let rec max
: type a b c.(a,b,c) max → a → b → c
= fun mx m n → match mx ,m with
MaxEq , _ → m
| MaxFlip mx ’, _ → max mx’ n m
| MaxSuc mx ’ , S m’ → S (max mx’ m’ n)
35/ 53
A typed maximum function
type (_,_,_) max =
MaxEq : (’a,’a,’a) max
| MaxFlip : (’a,’b,’c) max → (’b,’a,’c) max
| MaxSuc : (’a,’b,’a) max → (’a s,’b,’a s) max
let rec max : type a b c.(a,b,c) max → a → b → c
= fun mx m n → match mx ,m with
MaxEq , _ → m
| MaxFlip mx ’, _ → max mx’ n m
| MaxSuc mx ’ , S m’ → S (max mx’ m’ n)
Type refinement
In the MaxEq branch: a≡ b, a≡ c
m : c
In the MaxFlip branch: no refinement
In the MaxSuc branch: a≡ d s, c≡ d s (for some d)
mx’ : (d, b, d)max
m’ : d
max mx’ m’ n : d
36/ 53
Term inference for depth-annotated trees
val ? : (’a,’n) dtree → ’n
val ? : (’a,’n s) dtree → ’a
val ? : (’a,’n) dtree → (’a,’n) dtree
37/ 53
Depth-annotated trees: depth
T[3]
max(2,0)≡2 (p1)
T[2]
max(1,0)≡1 (p2)
T[1]
max(0,0)≡0 (p3)
E a E
b E
c E
S (max p1
(S (max p2
(S (max p3
Z
Z))
Z))
Z)
let rec depthD : type a n.(a,n) dtree → n =
function
EmptyD → Z
| TreeD (l,_,r,mx) → S (max mx (depthD l) (depthD r))
38/ 53
Depth-annotated trees: top
T[3]
max(2,0)≡2 (p1)
T[2]
max(1,0)≡1 (p2)
T[1]
max(0,0)≡0 (p3)
E a E
b E
c E
c
let topD : type a n.(a,n s) dtree → a =
function TreeD (_,v,_,_) → v
39/ 53
Depth-annotated trees: swivel
T[2]
max(1,0)≡1
T[1]
max(0,0)≡0
E a E
b E
T[2]
max(0,1)≡1
E b T[1]
max(0,0)≡0
E a E
let rec swivelD :
type a n.(a,n) dtree → (a,n) dtree =
function
EmptyD → EmptyD
| TreeD (l,v,r,m) →
TreeD (swivelD r, v, swivelD l, MaxFlip m)
40/ 53
Efficiency
41/ 53
Efficiency: missing branches
let top : ’a.’a tree → ’a option = function
Empty → None
| Tree (_,v,_) → Some v
(function p (* ocaml -dlambda *)
(if p
(makeblock 0 (field 1 p))
0a))
let topG : type a n.(a,n s) gtree → a = function
TreeG (_,v,_) → v
(function p (* ocaml -dlambda *)
(field 1 p))
42/ 53
Efficiency: zips
let rec zipTree :
type a b n.(a,n) gtree → (b,n) gtree →
(a * b,n) gtree =
fun x y → match x, y with
EmptyG , EmptyG → EmptyG
| TreeG (l,v,r), TreeG (m,w,s) →
TreeG (zipTree l m, (v,w), zipTree r s)
(letrec (* ocaml -dlambda *)
(zipTree
(function x y
(if x
(makeblock 0
(apply zipTree (field 0 x) (field 0 y))
(makeblock 0 (field 1 x) (field 1 y))
(apply zipTree (field 2 x) (field 2 y)))
0a)))
(apply (field 1 (global Toploop!)) “zipTree” zipTree))
43/ 53
Equality
44/ 53
Recall: equality in System Fω
Eql = λα::∗.λβ::∗.∀ϕ::∗ ⇒ ∗.ϕ α → ϕ β
refl : ∀α::∗.Eql α α
refl = Λα::∗.Λϕ::∗ ⇒ ∗.λx:ϕ α.x
symm : ∀α::∗.∀β::∗.Eql α β → Eql β α
symm = Λα::∗.Λβ::∗.
λe:(∀ϕ::∗ ⇒ ∗.ϕ α → ϕ β).e [λγ::∗.Eq γ α] (refl [α])
trans : ∀α::∗.∀β::∗.∀γ::∗.Eql α β → Eql β γ → Eql α γ
trans = Λα::∗.Λβ::∗.Λγ::∗.
λab:Eq α β.λbc:Eq β γ.bc [Eq α] ab
45/ 53
Equlity with GADTs
type (_, _) eql = Refl : (’a,’a) eql
val refl : (’a,’a) eql
val symm : (’a,’b) eql → (’b,’a) eql
val trans : (’a,’b) eql → (’b,’c) eql → (’a,’c) eql
module Lift (T : sig type _ t end) :
sig
val lift : (’a,’b) eql → (’a T.t,’b T.t) eql
end
val cast : (’a,’b) eql → ’a → ’b
46/ 53
Building GADTs from algebraic types and equality
type (’a, _) gtree =
EmptyG : (’a,z) gtree
| TreeG : (’a,’n) gtree * ’a * (’a,’n) gtree → (’a,’n s)
gtree
type (’a,’n) etree =
EmptyE : (z,’n) eql → (’a,’n) etree
| TreeE : (’n,’m s) eql *
(’a,’m) etree * ’a * (’a,’m) etree → (’a,’n) etree
47/ 53
Building GADTs from algebraic types and equality
type (’a, _) gtree =
EmptyG : (’a,z) gtree
| TreeG : (’a,’n) gtree * ’a * (’a,’n) gtree → (’a,’n s)
gtree
let rec depthG : type a n.(a, n) gtree → n =
function
EmptyG → Z
| TreeG (l,_,_) → S (depthG l)
48/ 53
Building GADTs from algebraic types and equality
type (’a, _) gtree =
EmptyG : (’a,z) gtree
| TreeG : (’a,’n) gtree * ’a * (’a,’n) gtree → (’a,’n s)
gtree
let rec depthG : type a n.(a, n) gtree → n =
function
EmptyG → Z (* n = z *)
| TreeG (l,_,_) → S (depthG l)
48/ 53
Building GADTs from algebraic types and equality
type (’a, _) gtree =
EmptyG : (’a,z) gtree
| TreeG : (’a,’n) gtree * ’a * (’a,’n) gtree → (’a,’n s)
gtree
let rec depthG : type a n.(a, n) gtree → n =
function
EmptyG → Z (* n = z *)
| TreeG (l,_,_) → S (depthG l) (* n = m s *)
48/ 53
Building GADTs from algebraic types and equality
type (’a,’n) etree =
EmptyE : (’n,z) eql → (’a,’n) etree
| TreeE : (’n,’m s) eql *
(’a,’m) etree * ’a * (’a,’m) etree → (’a,’n) etree
let rec depthE : type a n.(a, n) etree → n =
function
EmptyE Refl → Z
| TreeE (Refl , l,_,_) → S (depthE l)
49/ 53
Building GADTs from algebraic types and equality
type (’a,’n) etree =
EmptyE : (’n,z) eql → (’a,’n) etree
| TreeE : (’n,’m s) eql *
(’a,’m) etree * ’a * (’a,’m) etree → (’a,’n) etree
let rec depthE : type a n.(a, n) etree → n =
function
EmptyE Refl → Z (* n = z *)
| TreeE (Refl , l,_,_) → S (depthE l)
49/ 53
Building GADTs from algebraic types and equality
type (’a,’n) etree =
EmptyE : (’n,z) eql → (’a,’n) etree
| TreeE : (’n,’m s) eql *
(’a,’m) etree * ’a * (’a,’m) etree → (’a,’n) etree
let rec depthE : type a n.(a, n) etree → n =
function
EmptyE Refl → Z (* n = z *)
| TreeE (Refl , l,_,_) → S (depthE l) (* n = m s *)
49/ 53
Reorientation
50/ 53
Where are we?
We’ve enriched data types with indexes describing the data.
Families of types: a type for each nat, each tree depth, etc.
Descriptive data types lead to useful function types.
Phantom types protect abstractions against misuse.
GADTs also protect definitions.
Compilers use the extra information to generate better code.
51/ 53
What’s going on?
GADTs are about type equalities (and sometimes inequalities).
GADTs reveal things about types when you examine data.
We need machinery from earlier lectures: existentials,
polymorphic recursion, non-regularity.
GADTs lead to rich types which can be viewed as propositions.
Setting up types carefully leads to simple and fast code.
52/ 53
Next time
GADTs in practice
53/ 53