程序代写代做代考 ocaml Last time: GADTs

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