程序代写代做代考 ocaml Last time: monads (etc.)

Last time: monads (etc.)

>>= ⊗

1/ 43

This time: generic programming

val show : ’a → string

2/ 43

Generic functions

3/ 43

Data types

unit

type unit =

Unit : unit

booleans

type bool =

False: bool

| True : bool

natural numbers

type nat =

Zero: nat

| Succ: nat → nat

sums

type (’a,’b) sum =

Left : ’a → (’a,’b) sum
| Right: ’b → (’a,’b) sum

pairs

type (’a,’b) pair =

Pair: ’a * ’b → (’a,’b) pair

lists

type ’a list =

Nil : ’a list

| Cons: ’a * ’a list → ’a list

4/ 43

Data type operations: formatting

unit

let string_of_unit : unit → string = function
Unit → “Unit”

booleans

let string_of_bool : bool → string = function
False → “False”

| True → “True”

natural numbers

let rec string_of_nat : nat → string = function
Zero → “Zero”

| Succ n → “(Succ “^ string_of_nat n ^”)”

5/ 43

Data type operations: formatting (continued)

sums

let string_of_sum :

(’a → string) → (’b → string) → (’a,’b) sum → string =
fun l r → function

Left x → “(Left “^ l x ^”)”
| Right y → “( Right “^ r y ^”)”

pairs

let string_of_pair :

(’a → string) → (’b → string) → (’a,’b) pair → string =
fun l r → function

Pair (x, y) → “(Pair “^ l x ^”,”^ r y ^”)”

lists

let rec string_of_list :

(’a → string) → ’a list → string =
fun a → function

Nil → “Nil”
| Cons (x,xs) → “(Cons “^ a x ^”,”^ string_of_list a y ^”)”

6/ 43

Operations defined on (most) data

equality
’a → ’a → bool

hashing
’a → int

ordering
’a → ’a → int

mapping
(’b → ’b) → ’a → ’a

querying
(’b → bool) → ’a → ’b list

pretty-printing
’a → string

parsing
string → ’a

serialising
’a → string

sizing
’a → int

7/ 43

Generic functions and parametricity

Some built-in OCaml functions are incompatible with parametricity:

val (=) : ’a → ’a → bool

val hash : ’a → int

val from_string : string → int → ’a

8/ 43

Generic functions and parametricity

Some built-in OCaml functions are incompatible with parametricity:

val (=) : ’a → ’a → bool

val hash : ’a → int

val from_string : string → int → ’a

How might we do better? Pass a description of the data shape:

val (=) : {D:DATA} → D.t → D.t → bool

val hash : {D:DATA} → D.t → int

val from_string : {D:DATA} → string → int → D.t

9/ 43

Data shape descriptions: type-indexed values

Idea: give an instance of some signature T for each OCaml types:

module T_int : T with type t = int

module T_bool : T with type t = bool

module T_pair (A:T) (B:T) : T with type t = A.t * B.t

module T_list (A:T) : T with type t = A.t list

module T_option (A:T) : T with type t = A.t option

(* etc. *)

int is represented by a module
T_int : T with type t = int

int * bool is represented by a module
T_pair(T_int)(T_bool): T with type t = int * bool

int option list is represented by a module
T_list(T_option(T_int)): T with type t = int option list

(etc.)

10/ 43

Data as trees

L

()

L ()

,,,

10 20 30 40

(10 ,20 ,30 ,40)

::

,

1 ”one”

::

,

2 ”two”

::

,

3 ”three”

[]

[(1, “one”); (2, “two”); (3, “three “)]

11/ 43

Generic operations: three questions about data

1. What type is this data?

2. What are its subnodes?

3. What about the recursive case?

::

,

1 ”one”

::

,

2 ”two”

::

,

3 ”three”

[]

12/ 43

1. Examining types

13/ 43

Determining type equality

A type representation:

type _ type_rep

A type equality test that returns a proof on success:

val eqrep : ’a type_rep → ’b type_rep → (’a,’b) eql option

# eqrep ty_int ty_float

– : (int , float) eql option = None

# eqrep ty_int ty_int

– : (int , int) eql option = Some Refl

14/ 43

Type indexed values for type equality

module type TYPEABLE = sig

type t

val type_rep : t type_rep

val eqrep : ’other type_rep → (t, ’other) eql option
end

implicit module Typeable_int : TYPEABLE with type t = int

implicit module Typeable_bool : TYPEABLE with type t = bool

implicit module Typeable_list{A:TYPEABLE}

(* etc. *)

15/ 43

Representing types

How should we define type_rep?

type _ type_rep =

Int : int type_rep

| Bool : bool type_rep

| List : ’a type_rep → ’a list type_rep
| Option : ’a type_rep → ’a option type_rep
| Pair : ’a type_rep * ’b type_rep → (’a * ’b) type_rep

16/ 43

Implementing type equality

let rec eqrep :

type a b.a typerep → b typerep → (a,b) eql option =
fun l r → match l, r with

Int , Int → Some Refl
| Bool , Bool → Some Refl
| List s, List t →

(match eqrep s t with

Some Refl → Some Refl
| None → None)

| Option s, Option t →
(match eqrep s t with

Some Refl → Some Refl
| None → None)

| Pair (s1 , s2), Pair (t1, t2) →
(match eqrep s1 t1, eqrep s2 t2 with

Some Refl , Some Refl → Some Refl
| _ → None)

| _ → None

17/ 43

Implementing type equality

let rec eqrep :

type a b.a typerep → b typerep → (a,b) eql option =
fun l r → match l, r with

Int , Int → Some Refl
| Bool , Bool → Some Refl
| List s, List t →

(match eqrep s t with

Some Refl → Some Refl
| None → None)

| Option s, Option t →
(match eqrep s t with

Some Refl → Some Refl
| None → None)

| Pair (s1 , s2), Pair (t1, t2) →
(match eqrep s1 t1, eqrep s2 t2 with

Some Refl , Some Refl → Some Refl
| _ → None)

| _ → None

Problem: this representation has no support for user-defined types.

17/ 43

Extensible variants

Defining

type ’a t = ..

Extending

type ’a t +=

A : int list → int t
| B : float list → ’a t

Constructing

A [1;2;3] (* No different to standard variants *)

Matching

let f : type a. a t → string = function
A _ → “A”

| B _ → “B”
| _ → “unknown” (* All matches must be open *)

18/ 43

Representing types, extensibly

type _ type_rep = ..

type _ type_rep += List : ’a type_rep → ’a list type_rep

implicit module Typeable_list{A:TYPEABLE}

: TYPEABLE with type t = A.t list =

struct

type t = A.t list

let type_rep = List A.type_rep

let eqrep : type b.b type_rep → (A.t list ,b) eql option =
function

| List b → (match A.eqrep b with
Some Refl → Some Refl

| None → None)
| _ → None

end

19/ 43

Implementing type equality, extensibly

module type TYPEABLE = sig

type t

val type_rep : t type_rep

val eqrep : ’other type_rep → (t, ’other) eql option
end

val eqty : {A:TYPEABLE} → {B:TYPEABLE} →
(A.t, B.t) eq option

let eqty {A:TYPEABLE} {B:TYPEABLE} = A.eqrep B.type_rep

20/ 43

2. Accessing subnodes

21/ 43

Traversing datatypes

gmapT
a

b

e g h i

c d

j

a

f b

e g h i

f c f d

j

gmapQ
a

b

e g h i

c d

j

⇝ [q b; q c; q d]

22/ 43

An interface for accessing subnodes

module type DATA

type genericT = {D:DATA} → D.t → D.t
type ’u genericQ = {D:DATA} → D.t → ’u

val gmapT : genericT → genericT
val gmapQ : ’u genericQ → ’u list genericQ

23/ 43

A signature for accessing subnodes

module type DATA = sig

type t

module Typeable : TYPEABLE with type t = t

val gmapT : genericT → t → t
val gmapQ : ’u genericQ → t → ’u list

end

implicit module Data_int : DATA with type t = int

implicit module Data_list{A:DATA} : DATA with type t = A.t list

(etc.)

24/ 43

Polymorphic types for generic traversals: gmapT

a

b

e g h i

c d

j

a

f b

e g h i

f c f d

j

type genericT = {D:DATA} → D.t → D.t

val gmapT : genericT → genericT

25/ 43

Polymorphic types for generic queries: gmapQ

a

b

e g h i

c d

j

⇝ [q b; q c; q d]

type ’u genericQ = {D:DATA} → D.t → ’u

val gmapQ : ’u genericQ → ’u list genericQ

26/ 43

Traversing datatypes: primitive types

x ⇝ x

gmapT {Data_int} f

implicit module Data_int : DATA with type t = int =

struct

type t = int

module Typeable = Typeable_int

let gmapT f x = x

let gmapQ f x = []

end

27/ 43

Traversing datatypes: pairs

,

x y

,

f x f y

gmapT {Data_pair{A}{B}} f

With DATA instances A and B for the type parameters:

implicit module Data_pair {A: DATA} {B: DATA}

: DATA with type t = A.t * B.t =

struct

type t = A.t * B.t

module Typeable = Typeable_pair{A.Typeable }{B.Typeable}

let gmapT f (x, y) = (f x, f y)

let gmapQ q (x, y) = [q x; q y]

end

28/ 43

Traversing datatypes: lists
::

w ::

x ::

y ::

z []

::

f w f ::

x ::

y ::

z []

gmapT (list a)f

implicit module rec Data_list {A: DATA} :

DATA with type t = A.t list = struct

type t = A.t list

module Typeable = Typeable_list{A.Typeable}

let gmapT f l =

match l with [] → [] | x :: xs → f x :: f xs
let gmapQ q l =

match l with [] → [] | x :: xs → [q x; q xs]
end

(Disclaimer: implicit module rec not yet supported)

29/ 43

3. Handling recursion

30/ 43

Generic maps, bottom up

let rec everywhere : genericT → genericT =
fun f {X:DATA} x → f (gmapT (everywhere f) x)

In practice a few more annotations are needed:

let rec everywhere : genericT → genericT =
fun (f : genericT) {X:DATA} x →

f ((gmapT (everywhere f) : genericT) x)

31/ 43

Generic maps, top down

let rec everywhere ’ : genericT → genericT =
fun f {X:DATA} x → gmapT (everywhere ’ f) (f x)

With annotations:

let rec everywhere ’ : genericT → genericT =
fun (f : genericT) {X:DATA} x →

(gmapT (everywhere ’ f) : genericT) (f {X} x)

32/ 43

Generic maps with a stop condition

val everywhereBut : bool genericQ → genericT → genericT

let rec everywhereBut :

bool genericQ → genericT → genericT =
fun stop f {X:DATA} x →

if stop x then x

else f (gmapT (everywhereBut stop f) x)

33/ 43

Using generic maps

val everywhere : genericT → genericT

let mkT : {T:TYPEABLE} → (T.t → T.t) → genericT =
fun {T:TYPEABLE} g {D: DATA} x →

match eqty {T} {D:TYPEABLE} with

| Some Refl → g x
| None → x

(In practice, we need an auxiliary function: see the notebook.)

everywhere (mkT succ) [(false , 1); (false , 2); (true , 3)]

34/ 43

Generic queries

let rec everything : ’r. (’r → ’r → ’r) → ’r genericQ → ’
r genericQ =

fun join g {X: DATA} x →
fold_left join (g x)

(gmapQ (everything join g) x)

let rec everythingBut :

’r. (’r → ’r → ’r) → (’r * bool) genericQ → ’r genericQ =
fun join stop {X: DATA} x →

match stop x with

| v, true → v
| v, false → fold_left join v

(gmapQ (everythingBut join stop) x)

35/ 43

Using generic queries

val everything :

(’r → ’r → ’r) → ’r genericQ → ’r genericQ =

let mkQ : ’u. {T:TYPEABLE} → ’u → (T.t → ’u) → ’u genericQ =
fun {T:TYPEABLE} u g {D: DATA} x →
match eqty {T} {D.Typeable} with

| Some Refl → g x
| None → u

everything (@) (mkQ [] (fun x → [x])) [(1, false); (2,true)]

36/ 43

Generic printing

37/ 43

Representing constructors

Add an additional field to data for distinguishing constructors:

module type DATA = sig

type t

module Typeable : TYPEABLE with type t = t

val gmapT : genericT → t → t
val gmapQ : ’u genericQ → t → ’u list
val constructor_: t → string

end

38/ 43

A generic printing function

a

b

e g h i

c d

j

⇝ “(a (b (e) (g) (h) (i)) (c) (d (j)))”

let rec gshow {D:DATA} (v : D.t) =

“(“^ constructor_ v ^ String.concat ” ” (gmapQ gshow v) ^ “)”

39/ 43

Generic sizing

40/ 43

Computing value size generically

a

b

e g h i

c d

j

⇝ 9

let sum l = List.fold_left (+) 0 l

let rec gsize {D:DATA} (v : D.t) = 1 + sum (gmapQ gsize v)

gsize 3

gsize [1;2;3]

gsize [(1, false); (2,false); (3,true)]

41/ 43

Main remaining problem: performance

Generic traversals are slow!

Solution: staging (next week)

.< e >.

42/ 43

Next time: monads (etc.), continued

>>= ⊗ effect E

43/ 43