Last time: GADTs
a ≡ b
1/ 47
This time: GADT programming patterns
2/ 47
Recap: 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
3/ 47
Functions on depth-annotated trees
val ? : (’a,’n) dtree → ’n
val ? : (’a,’n s) dtree → ’a
val ? : (’a,’n) dtree → (’a,’n) dtree
4/ 47
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))
5/ 47
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
6/ 47
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)
7/ 47
Recapitulation
8/ 47
Recapitulation: philosophical
Phantom types protect abstractions against misuse.
GADTs also protect definitions.
GADTs lead to rich types which can be viewed as propositions.
Descriptive data types lead to useful function types.
9/ 47
Recapitulation: technical
GADT type indexes vary across constructors.
We have families of types: a type per nat, per tree depth, etc.
GADTs need machinery from earlier lectures: existentials,
polymorphic recursion, non-regularity.
GADTs are about type equalities (and sometimes inequalities).
Type equalities are revealed by examining data.
Compilers use the richer types to generate better code.
10/ 47
Efficiency
11/ 47
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))
12/ 47
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))
13/ 47
Equality
14/ 47
Recall: equality in System Fω
Eq = λα::∗.λβ::∗.∀ϕ::∗ ⇒ ∗.ϕ α → ϕ β
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
15/ 47
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
16/ 47
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
17/ 47
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)
18/ 47
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)
18/ 47
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 *)
18/ 47
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)
19/ 47
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)
19/ 47
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 *)
19/ 47
GADT programming patterns
20/ 47
A new example: representing (some) JSON
JSON values
json ::= true | false | string | number | null
[] | [ json-seq ]
{} | { json-kvseq }
json-seq ::= json
json , json-seq
json-kvseq ::= string : json
string : json , json-kvseq
21/ 47
A new example: representing (some) JSON
JSON values
json ::= true | false | string | number | null
[] | [ json-seq ]
json-seq ::= json
json , json-seq
A JSON value
[ “one”, true , 3.4, [[ “four” ], [null ]]]
22/ 47
An “untyped” JSON representation
type ujson =
UStr : string → ujson
| UNum : float → ujson
| UBool : bool → ujson
| UNull : ujson
| UArr: ujson list → ujson
[ “one”, true , 3.4, [[ “four” ], [null ]]]
UArr [UStr “one”; UBool true; UNum 3.4;
UArr [UArr [UStr “four “]; UArr [UNull ]]]
23/ 47
Pattern: Richly typed data
Data may have finer structure than algebraic data types can express.
GADT indexes allow us to specify constraints more precisely.
24/ 47
Richly typed data
type _ tjson =
Str : string → string tjson
| Num : float → float tjson
| Bool : bool → bool tjson
| Null : unit tjson
| Arr : ’a tarr → ’a tjson
and _ tarr =
Nil : unit tarr
| :: : ’a tjson * ’b tarr → (’a*’b) tarr
Arr (Str “one” :: Bool true :: Num 3.4 ::
Arr (Arr (Str “four” :: Nil) :: Null :: Nil) :: Nil)
25/ 47
Richly typed data
(* negate all the bools in a JSON value *)
let rec unegate : ujson → ujson = . . .
(* negate all the bools in a JSON value *)
let rec negate : type a.a tjson → a tjson = function
Bool true → Bool false
| Bool false → Bool true
| Arr arr → Arr (negate_arr arr)
| v → v
and negate_arr : type a.a tarr → a tarr = function
Nil → Nil
| j :: js → negate j :: negate_arr js
26/ 47
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.
27/ 47
Building GADT values: two approaches
How might a function make_t build a value of a GADT type _ t?
let make_t : type a.string → a t = . . .
With existentials make_t builds a value of type ’a t for some ’a.
With universals the caller of make_t must accept ’a t for any ’a.
28/ 47
Building GADT values: two approaches
How might a function make_t build a value of a GADT type _ t?
let make_t : type a.string → a t = 7
With existentials make_t builds a value of type ’a t for some ’a.
With universals the caller of make_t must accept ’a t for any ’a.
28/ 47
Building GADT values: two approaches
How might a function make_t build a value of a GADT type _ t?
let make_t : type a.string → a t = 7
With existentials make_t builds a value of type ’a t for some ’a.
With universals the caller of make_t must accept ’a t for any ’a.
28/ 47
Building GADT values: two approaches
How might a function make_t build a value of a GADT type _ t?
let make_t : type a.string → a t = 7
With existentials make_t builds a value of type ’a t for some ’a.
With universals the caller of make_t must accept ’a t for any ’a.
28/ 47
Building GADT values with existentials
type etjson = ETJson : ’a tjson → etjson
type etarr = ETArr : ’a tarr → etarr
let rec tjson_of_ujson : ujson → etjson = function
UStr s → ETJson (Str s)
| UNum u → ETJson (Num u)
| UBool b → ETJson (Bool b)
| UNull → ETJson Null
| UArr arr →
let ETArr arr ’ = tarr_of_uarr arr in
ETJson (Arr arr ’)
and tarr_of_uarr : ujson list → etarr = function
[] → ETArr Nil
| j :: js →
let ETJson j’ = tjson_of_ujson j in
let ETArr js ’ = tarr_of_uarr js in
ETArr (j’ :: js ’)
29/ 47
Building GADT values with existentials
type etjson = ETJson : ’a tjson → etjson
type etarr = ETArr : ’a tarr → etarr
let rec tjson_of_ujson : ujson → etjson = function
UStr s → ETJson (Str s)
(* Str s : string tjson *)
| UNum u → ETJson (Num u)
| UBool b → ETJson (Bool b)
| UNull → ETJson Null
| UArr arr →
let ETArr arr ’ = tarr_of_uarr arr in
ETJson (Arr arr ’)
and tarr_of_uarr : ujson list → etarr = function
[] → ETArr Nil
| j :: js →
let ETJson j’ = tjson_of_ujson j in
let ETArr js ’ = tarr_of_uarr js in
ETArr (j’ :: js ’)
29/ 47
Building GADT values with existentials
type etjson = ETJson : ’a tjson → etjson
type etarr = ETArr : ’a tarr → etarr
let rec tjson_of_ujson : ujson → etjson = function
UStr s → ETJson (Str s)
(* Str s : string tjson *)
| UNum u → ETJson (Num u) (* Num u : float tjson *)
| UBool b → ETJson (Bool b)
| UNull → ETJson Null
| UArr arr →
let ETArr arr ’ = tarr_of_uarr arr in
ETJson (Arr arr ’)
and tarr_of_uarr : ujson list → etarr = function
[] → ETArr Nil
| j :: js →
let ETJson j’ = tjson_of_ujson j in
let ETArr js ’ = tarr_of_uarr js in
ETArr (j’ :: js ’)
29/ 47
Building GADT values with existentials
type etjson = ETJson : ’a tjson → etjson
type etarr = ETArr : ’a tarr → etarr
let rec tjson_of_ujson : ujson → etjson = function
UStr s → ETJson (Str s)
(* Str s : string tjson *)
| UNum u → ETJson (Num u) (* Num u : float tjson *)
| UBool b → ETJson (Bool b) (* Bool b : bool tjson *)
| UNull → ETJson Null
| UArr arr →
let ETArr arr ’ = tarr_of_uarr arr in
ETJson (Arr arr ’)
and tarr_of_uarr : ujson list → etarr = function
[] → ETArr Nil
| j :: js →
let ETJson j’ = tjson_of_ujson j in
let ETArr js ’ = tarr_of_uarr js in
ETArr (j’ :: js ’)
29/ 47
Building GADT values with existentials
type etjson = ETJson : ’a tjson → etjson
type etarr = ETArr : ’a tarr → etarr
let rec tjson_of_ujson : ujson → etjson = function
UStr s → ETJson (Str s)
(* Str s : string tjson *)
| UNum u → ETJson (Num u) (* Num u : float tjson *)
| UBool b → ETJson (Bool b) (* Bool b : bool tjson *)
| UNull → ETJson Null (* Null : unit tjson *)
| UArr arr →
let ETArr arr ’ = tarr_of_uarr arr in
ETJson (Arr arr ’)
and tarr_of_uarr : ujson list → etarr = function
[] → ETArr Nil
| j :: js →
let ETJson j’ = tjson_of_ujson j in
let ETArr js ’ = tarr_of_uarr js in
ETArr (j’ :: js ’)
29/ 47
Building GADT values with existentials
type etjson = ETJson : ’a tjson → etjson
type etarr = ETArr : ’a tarr → etarr
let rec tjson_of_ujson : ujson → etjson = function
UStr s → ETJson (Str s)
(* Str s : string tjson *)
| UNum u → ETJson (Num u) (* Num u : float tjson *)
| UBool b → ETJson (Bool b) (* Bool b : bool tjson *)
| UNull → ETJson Null (* Null : unit tjson *)
| UArr arr → (* arr’ : ?a tarr *)
let ETArr arr ’ = tarr_of_uarr arr in
ETJson (Arr arr ’)
and tarr_of_uarr : ujson list → etarr = function
[] → ETArr Nil
| j :: js →
let ETJson j’ = tjson_of_ujson j in
let ETArr js ’ = tarr_of_uarr js in
ETArr (j’ :: js ’)
29/ 47
Building GADT values with existentials
type etjson = ETJson : ’a tjson → etjson
type etarr = ETArr : ’a tarr → etarr
let rec tjson_of_ujson : ujson → etjson = function
UStr s → ETJson (Str s)
(* Str s : string tjson *)
| UNum u → ETJson (Num u) (* Num u : float tjson *)
| UBool b → ETJson (Bool b) (* Bool b : bool tjson *)
| UNull → ETJson Null (* Null : unit tjson *)
| UArr arr → (* arr’ : ?a tarr *)
let ETArr arr ’ = tarr_of_uarr arr in
ETJson (Arr arr ’) (* Arr arr’ : ?a tjson *)
and tarr_of_uarr : ujson list → etarr = function
[] → ETArr Nil
| j :: js →
let ETJson j’ = tjson_of_ujson j in
let ETArr js ’ = tarr_of_uarr js in
ETArr (j’ :: js ’)
29/ 47
Building GADT values with universals
type ’k atjson = {k: ’a. ’a tjson → ’k}
type ’k atarr = {k: ’a. ’a tarr → ’k}
let rec tjson_of_ujson : ujson → ’k atjson → ’k =
fun j {k=return} → match j with
UStr s → return (Str s)
| UNum u → return (Num u)
| UBool b → return (Bool b)
| UNull → return Null
| UArr arr →
tarr_of_uarr arr {k = fun arr ’ →
return (Arr arr ’) }
and tarr_of_uarr : ujson list → ’k atarr → ’k =
fun jl {k=return} → match jl with
[] → return Nil
| j :: js →
tjson_of_ujson j {k = fun j’ →
tarr_of_uarr js {k = fun js ’ →
return (j’ :: js ’) }}
30/ 47
Building GADT values with universals
type ’k atjson = {k: ’a. ’a tjson → ’k}
type ’k atarr = {k: ’a. ’a tarr → ’k}
let rec tjson_of_ujson : ujson → ’k atjson → ’k =
fun j {k=return} → match j with
UStr s → return (Str s)
(* Str s : string tjson *)
| UNum u → return (Num u)
| UBool b → return (Bool b)
| UNull → return Null
| UArr arr →
tarr_of_uarr arr {k = fun arr ’ →
return (Arr arr ’) }
and tarr_of_uarr : ujson list → ’k atarr → ’k =
fun jl {k=return} → match jl with
[] → return Nil
| j :: js →
tjson_of_ujson j {k = fun j’ →
tarr_of_uarr js {k = fun js ’ →
return (j’ :: js ’) }}
30/ 47
Building GADT values with universals
type ’k atjson = {k: ’a. ’a tjson → ’k}
type ’k atarr = {k: ’a. ’a tarr → ’k}
let rec tjson_of_ujson : ujson → ’k atjson → ’k =
fun j {k=return} → match j with
UStr s → return (Str s)
(* Str s : string tjson *)
| UNum u → return (Num u) (* Num u : float tjson *)
| UBool b → return (Bool b)
| UNull → return Null
| UArr arr →
tarr_of_uarr arr {k = fun arr ’ →
return (Arr arr ’) }
and tarr_of_uarr : ujson list → ’k atarr → ’k =
fun jl {k=return} → match jl with
[] → return Nil
| j :: js →
tjson_of_ujson j {k = fun j’ →
tarr_of_uarr js {k = fun js ’ →
return (j’ :: js ’) }}
30/ 47
Building GADT values with universals
type ’k atjson = {k: ’a. ’a tjson → ’k}
type ’k atarr = {k: ’a. ’a tarr → ’k}
let rec tjson_of_ujson : ujson → ’k atjson → ’k =
fun j {k=return} → match j with
UStr s → return (Str s)
(* Str s : string tjson *)
| UNum u → return (Num u) (* Num u : float tjson *)
| UBool b → return (Bool b) (* Bool b : bool tjson *)
| UNull → return Null
| UArr arr →
tarr_of_uarr arr {k = fun arr ’ →
return (Arr arr ’) }
and tarr_of_uarr : ujson list → ’k atarr → ’k =
fun jl {k=return} → match jl with
[] → return Nil
| j :: js →
tjson_of_ujson j {k = fun j’ →
tarr_of_uarr js {k = fun js ’ →
return (j’ :: js ’) }}
30/ 47
Building GADT values with universals
type ’k atjson = {k: ’a. ’a tjson → ’k}
type ’k atarr = {k: ’a. ’a tarr → ’k}
let rec tjson_of_ujson : ujson → ’k atjson → ’k =
fun j {k=return} → match j with
UStr s → return (Str s)
(* Str s : string tjson *)
| UNum u → return (Num u) (* Num u : float tjson *)
| UBool b → return (Bool b) (* Bool b : bool tjson *)
| UNull → return Null (* Null : unit tjson *)
| UArr arr →
tarr_of_uarr arr {k = fun arr ’ →
return (Arr arr ’) }
and tarr_of_uarr : ujson list → ’k atarr → ’k =
fun jl {k=return} → match jl with
[] → return Nil
| j :: js →
tjson_of_ujson j {k = fun j’ →
tarr_of_uarr js {k = fun js ’ →
return (j’ :: js ’) }}
30/ 47
Building GADT values with universals
type ’k atjson = {k: ’a. ’a tjson → ’k}
type ’k atarr = {k: ’a. ’a tarr → ’k}
let rec tjson_of_ujson : ujson → ’k atjson → ’k =
fun j {k=return} → match j with
UStr s → return (Str s)
(* Str s : string tjson *)
| UNum u → return (Num u) (* Num u : float tjson *)
| UBool b → return (Bool b) (* Bool b : bool tjson *)
| UNull → return Null (* Null : unit tjson *)
| UArr arr → (* arr’ : ?a tarr *)
tarr_of_uarr arr {k = fun arr ’ →
return (Arr arr ’) }
and tarr_of_uarr : ujson list → ’k atarr → ’k =
fun jl {k=return} → match jl with
[] → return Nil
| j :: js →
tjson_of_ujson j {k = fun j’ →
tarr_of_uarr js {k = fun js ’ →
return (j’ :: js ’) }}
30/ 47
Building GADT values with universals
type ’k atjson = {k: ’a. ’a tjson → ’k}
type ’k atarr = {k: ’a. ’a tarr → ’k}
let rec tjson_of_ujson : ujson → ’k atjson → ’k =
fun j {k=return} → match j with
UStr s → return (Str s)
(* Str s : string tjson *)
| UNum u → return (Num u) (* Num u : float tjson *)
| UBool b → return (Bool b) (* Bool b : bool tjson *)
| UNull → return Null (* Null : unit tjson *)
| UArr arr → (* arr’ : ?a tarr *)
tarr_of_uarr arr {k = fun arr ’ →
return (Arr arr ’) } (* Arr arr’ : ?a tjson *)
and tarr_of_uarr : ujson list → ’k atarr → ’k =
fun jl {k=return} → match jl with
[] → return Nil
| j :: js →
tjson_of_ujson j {k = fun j’ →
tarr_of_uarr js {k = fun js ’ →
return (j’ :: js ’) }}
30/ 47
Pattern: Singleton types
Without dependent types we can’t write predicates involving data.
Using one type per value allows us to simulate value indexing.
31/ 47
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
32/ 47
Singleton types
type z = Z
type _ s = S : ’n → ’n s
type (_,_,_) max =
MaxEq : (’a,’b) eql → (’a,’b,’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
33/ 47
Pattern: Separating types and data
Entangling proofs and data can lead to redundant, inefficient code.
Separate proofs make data reusable and help avoid slow traversals.
34/ 47
Separating types and data
type _ tyjson =
TyStr : string tyjson
| TyNum : float tyjson
| TyBool : bool tyjson
| TyNull : ’a tyjson → ’a option tyjson
| TyArr: ’a tyarr → ’a tyjson
and _ tyarr =
TyNil : unit tyarr
| :: : ’a tyjson * ’b tyarr → (’a * ’b) tyarr
Entangled
Arr (Str “one” :: Bool true :: Num 3.4 ::
Arr (Arr (Str “four” :: Nil) :: Null :: Nil) :: Nil)
Disentangled
TyArr (TyStr :: TyBool :: TyNum ::
TyArr (TyArr (TyStr :: TyNil)
:: TyNull TyBool :: TyNil) :: TyNil)
(“one”, (true , (3.4, ((((” four”, ()), (None , ())), ())
))))
35/ 47
Separating types and data
The negate function, entangled
let rec negate : type a.a tjson → a tjson = function
Bool true → Bool false
| Bool false → Bool true
| Arr arr → Arr (negate_arr arr)
| v → v
and negate_arr : type a.a tarr → a tarr = function
Nil → Nil
| j :: js → negate j :: negate_arr js
36/ 47
Separating types and data
The negate function, disentangled
let rec negateD : type a.a tyjson → a → a =
fun t v → match t, v with
TyBool , true → false
| TyBool , false → true
| TyArr a, arr → negate_arrD a arr
| _, v → v
and negate_arrD : type a.a tyarr → a → a =
fun t v → match t, v with
TyNil , () → ()
| j :: js, (a, b) → (negateD j a, negate_arrD js b)
37/ 47
Separating types and data
The negate function, disentangled and “staged”
let rec negateDS : type a.a tyjson → a → a =
function
TyBool → (function false → true
| true → false)
| TyArr a → negate_arrDS a
| _ → (fun v → v)
and negate_arrDS : type a.a tyarr → a → a = function
TyNil → (fun () → ())
| j :: js → let n = negateDS j
and ns = negate_arrDS js in
(fun (a, b) → (n a, ns b))
38/ 47
Separating types and data: verifying data
let rec unpack_ujson :
type a.a tyjson → ujson → a option =
fun ty v → match ty , v with
TyStr , UStr s → Some s
| TyNum , UNum u → Some u
| TyBool , UBool b → Some b
| TyNull _, UNull → Some None
| TyNull j, v → (match unpack_ujson j v with
Some v → Some (Some v)
| None → None)
| TyArr a, UArr arr → unpack_uarr a arr
| _ → None
and unpack_uarr :
type a.a tyarr → ujson list → a option =
fun ty v → match ty , v with
TyNil , [] → Some ()
| j :: js, v :: vs →
(match unpack_ujson j v, unpack_uarr js vs with
Some v’, Some vs ’ → Some (v’, vs ’)
| _ → None)
| _ → None
39/ 47
Pattern: Building evidence
With type refinement we learn about types by inspecting values.
Predicates should return useful evidence rather than true or false.
40/ 47
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
41/ 47
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
42/ 47
Building evidence: JSON
Representing types built from strings and arrays
type _ str_tyjs =
SStr : string str_tyjs
| SArr : ’a str_tyarr → ’a str_tyjs
and ’a str_tyarr =
SNil : unit str_tyarr
| :: : ’a str_tyjs * ’b str_tyarr → (’a*’b) str_tyarr
43/ 47
Building evidence: JSON
Determining whether a type is built from strings and arrays
let rec is_stringy : type a.a tyjson → a str_tyjs option
=
function
TyStr → Some SStr
| TyNum → None
| TyBool → None
| TyNull _ → None
| TyArr arr → match is_stringy_array arr with
None → None
| Some sarr → Some (SArr sarr)
and is_stringy_array :
type a.a tyarr → a str_tyarr option =
function
TyNil → Some SNil
| x :: xs →
match is_stringy x, is_stringy_array xs with
Some x, Some xs → Some (x :: xs)
| _ → None
44/ 47
Building evidence: JSON (entangled)
Determining whether a value is built from strings and arrays
let rec is_stringyV : type a.a tjson → a str_tyjs option
=
function
Str _ → Some SStr
| Num _ → None
| Bool _ → None
| Null → None
| Arr arr → match is_stringy_arrayV arr with
None → None
| Some sarr → Some (SArr sarr)
and is_stringy_arrayV :
type a.a tarr → a str_tyarr option =
function
Nil → Some SNil
| x :: xs →
match is_stringyV x, is_stringy_arrayV xs with
Some x, Some xs → Some (x :: xs)
| _ → None
45/ 47
Summary
Richly typed data
Building GADT values
Singleton types
Separating types and data
Building evidence
46/ 47
Next time: monads etc.
>>=
47/ 47