Last time: GADTs
a ≡ b
1/ 28
This time: some GADT programming patterns
2/ 28
Term inference for depth-annotated trees
type (’a,_) dtree =
EmptyD : (’a,z) dtree
| TreeD : (’a,’m) dtree
* ’a
* (’a,’n) dtree
* (’m,’n,’o) max
→ (’a,’o s) dtree
val ? : (’a,’n) dtree → ’n
val ? : (’a,’n s) dtree → ’a
val ? : (’a,’n) dtree → (’a,’n) dtree
3/ 28
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))
4/ 28
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
5/ 28
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)
6/ 28
Efficiency
7/ 28
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))
8/ 28
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))
9/ 28
Equality
10/ 28
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
11/ 28
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
12/ 28
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
13/ 28
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)
14/ 28
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)
14/ 28
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 *)
14/ 28
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)
15/ 28
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)
15/ 28
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 *)
15/ 28
Some GADT programming patterns
16/ 28
Pattern: Building GADT values
It’s not always possible to determine index types statically.
For example, the depth of a tree might depend on user input.
17/ 28
Building GADT values: two approaches
How might mk_dtree build a value of the GADT type (’a,’n)dtree?
let mk_dtree
: type a n.a option → (a, n) dtree
= . . .
With existentials:
mk_dtree builds a value of type ’a dtree for some ’n.
With universals:
the caller of mk_dtree must accept (’a,’n)t for any ’n.
18/ 28
Building GADT values: two approaches
How might mk_dtree build a value of the GADT type (’a,’n)dtree?
let mk_dtree
: type a n.a option → (a, n) dtree
= 7
With existentials:
mk_dtree builds a value of type ’a dtree for some ’n.
With universals:
the caller of mk_dtree must accept (’a,’n)t for any ’n.
18/ 28
Building GADT values: two approaches
How might mk_dtree build a value of the GADT type (’a,’n)dtree?
let mk_dtree
: type a n.a option → (a, n) dtree
= 7
With existentials:
mk_dtree builds a value of type (’a,’n)dtree for some ’n.
With universals:
the caller of mk_dtree must accept (’a,’n)t for any ’n.
18/ 28
Building GADT values: two approaches
How might mk_dtree build a value of the GADT type (’a,’n)dtree?
let mk_dtree
: type a n.a option → (a, n) dtree
= 7
With existentials:
mk_dtree builds a value of type (’a,’n)dtree for some ’n.
With universals:
the caller of make_dtree must accept (’a, ’n)dtree for any ’n.
18/ 28
Building GADT values with existentials
type ’a edtree = E : (’a, ’n) dtree → ’a edtree
let mk_dtree : type a n. a option → a edtree =
function
None → E EmptyD
| Some v → E (TreeD (EmptyD , v, EmptyD , MaxEq Z))
19/ 28
Building GADT values with universals
type (’a, ’k) adtree = { k: ’n. (’a, ’n) dtree → ’k }
let mk_dtree_k: type a k.a option → (a, k) adtree → k =
fun opt {k} → match opt with
None → k EmptyD
| Some v → k (TreeD (EmptyD , v, EmptyD , MaxEq Z))
20/ 28
Pattern: Singleton types
Without dependent types we can’t write predicates involving data.
Using one type per value allows us to simulate value indexing.
21/ 28
Singleton types: Lambda and logic cubes
Fω // λC
F
??�������
// λP2
??�������
λω //
OO
λPω
OO
λ→ //
??������
OO
λP
??������
OO
propω // predω
prop2
??�������
// pred2
??�������
propω //
OO
predω
OO
prop //
??������
OO
pred
??������
OO
Singleton sets bring propositional logic closer to predicate logic.
∀A.B ∀{x}.B ∀x ∈ A.B
22/ 28
Singleton types
type z = Z
type _ s = S : ’n → ’n s
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
type (_,_,_) add =
AddZ : (z,’n,’n) add
| AddS : (’m,’n,’o) add → (’m s,’n,’o s) add
23/ 28
Pattern: Building evidence
With type refinement we learn about types by inspecting values.
Predicates should return useful evidence rather than true or false.
24/ 28
Building evidence: predicates returning bool
let is_empty : ’a .’a tree → bool = function
Empty → true
| Tree _ → false
if not (is_empty t) then
top t
else
None
25/ 28
Building evidence: trees
type _ is_zero =
Is_zero : z is_zero
| Is_succ : _ s is_zero
let is_empty : type a n.(a,n) dtree → n is_zero =
function
| EmptyD → Is_zero
| TreeD _ → Is_succ
match is_empty t with
| Is_succ → Some (topD t)
| Is_zero → None
26/ 28
Summary
Building GADT values
Singleton types
Building evidence
27/ 28
Next time: overloading
val (=) : {E:EQ} → E.t → E.t → bool
28/ 28