程序代写代做代考 ocaml Last time: generic programming

Last time: generic programming

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

1/ 55

This time: monads etc., continued

>>= ⊗ effect E

2/ 55

Recap: monads, bind and let

An imperative program

let id = !counter in

let () = counter := id + 1 in

string_of_int id

A monadic program

get >>= fun id →
put (id + 1) >>= fun () →

return (string_of_int id)

3/ 55

Recap: Higher-order effects with monads

val composeM :

(’a → ’b t) → (’b → ’c t) → (’a → ’c t)

let composeM f g x =

f x >>= fun y →
g y

val uncurryM :

(’a → (’b → ’c t) t) → ((’a * ’b) → ’c t)

let uncurryM f (x,y) =

f x >>= fun g →
g y

4/ 55

Applicatives
(let x = e . . . and)

5/ 55

Applicative programs

An imperative program

let x = fresh_name ()

and y = fresh_name ()

in (x, y)

An applicative program

pure (fun x y → (x, y))
⊗ fresh_name
⊗ fresh_name

6/ 55

Applicatives

module type APPLICATIVE =

sig

type ’a t

val pure : ’a → ’a t
val (⊗) : (’a → ’b) t → ’a t → ’b t

end

let pure {A:APPLICATIVE} x = A.pure x

let (⊗) {A:APPLICATIVE} m k = A.(⊗) m k

7/ 55

Applicatives

module type APPLICATIVE =

sig

type ’a t

val pure : ’a → ’a t
val (⊗) : (’a → ’b) t → ’a t → ’b t

end

let pure {A:APPLICATIVE} x = A.pure x

let (⊗) {A:APPLICATIVE} m k = A.(⊗) m k

Laws:

pure f ⊗ pure v ≡ pure (f v)
u ≡ pure id ⊗ u

u ⊗ (v ⊗ w) ≡ pure compose ⊗ u ⊗ v ⊗ w
v ⊗ pure x ≡ pure (fun f → f x) ⊗ v

7/ 55

>>= vs ⊗

The type of >>=: ’a t → (’a → ’b t) → ’b t

’a → ’b t: a function that builds a computation

(Almost) the type of ⊗: ’a t → (’a → ’b) t → ’b t

(’a → ’b) t: a computation that builds a function

The actual type of ⊗: (’a → ’b) t → ’a t → ’b t

8/ 55

Applicative normal forms

pure f ⊗ c1 ⊗ c2 . . . ⊗ cn

pure (fun x1 x2 . . . xn → e) ⊗ c1 ⊗ c2 . . . ⊗ cn

let x1 = c1
and x2 = c2
. . .

and xn = cn
in e

9/ 55

Applicative normalisation via the laws

pure f ⊗ (pure g ⊗ fresh_name) ⊗ fresh_name

10/ 55

Applicative normalisation via the laws

pure f ⊗ (pure g ⊗ fresh_name) ⊗ fresh_name
≡ (composition law)

(pure compose ⊗ pure f ⊗ pure g ⊗ fresh_name) ⊗ fresh_name

10/ 55

Applicative normalisation via the laws

pure f ⊗ (pure g ⊗ fresh_name) ⊗ fresh_name
≡ (composition law)

(pure compose ⊗ pure f ⊗ pure g ⊗ fresh_name) ⊗ fresh_name
≡ (homomorphism law (×2))

pure (compose f g) ⊗ fresh_name ⊗ fresh_name

10/ 55

Creating applicatives: every monad is an applicative

implicit module Applicative_of_monad {M:MONAD} :

APPLICATIVE with type ’a t = ’a M.t =

struct

type ’a t = ’a M.t

let pure = M.return

let (⊗) f p =
M.(f >>= fun g →

p >>= fun q →
return (g q))

end

11/ 55

The state applicative via the state monad

module StateA(S : sig type t end) :

sig

type state = S.t

type ’a t

module Applicative : APPLICATIVE with type ’a t = ’a t

val get : state t

val put : state → unit t
val runState : ’a t → state → state * ’a

end =

struct

type state = S.t

module StateM = State(S)

type ’a t = ’a StateM.t

module Applicative =

Applicative_of_monad{StateM.Monad}

let (get , put , runState) = StateM .(get , put , runState)

end

12/ 55

Creating applicatives: composing applicatives

module Compose (F : APPLICATIVE)

(G : APPLICATIVE) :

APPLICATIVE with type ’a t = ’a G.t F.t =

struct

type ’a t = ’a G.t F.t

let pure x = F.pure (G.pure x)

let (⊗) f x = F.(pure G.(⊗) ⊗ f ⊗ x)
end

13/ 55

Creating applicatives: the dual applicative

module Dual_applicative (A: APPLICATIVE)

: APPLICATIVE with type ’a t = ’a A.t =

struct

type ’a t = ’a A.t

let pure = A.pure

let (⊗) f x =
A.(pure (fun y g → g y) ⊗ x ⊗ f)

end

module RevNameA = Dual_applicative(NameA.Applicative)

RevNameA .(pure (fun x y → (x, y))
⊗ fresh_name
⊗ fresh_name)

14/ 55

Composed applicatives are law-abiding

pure f ⊗ pure x

15/ 55

Composed applicatives are law-abiding

pure f ⊗ pure x
≡ (definition of ⊗ and pure)

F.pure (⊗G ) ⊗F F.pure (G.pure f) ⊗F F.pure (G.pure x)

15/ 55

Composed applicatives are law-abiding

pure f ⊗ pure x
≡ (definition of ⊗ and pure)

F.pure (⊗G ) ⊗F F.pure (G.pure f) ⊗F F.pure (G.pure x)
≡ (homomorphism law for F (×2))

F.pure (G.pure f ⊗G G.pure x)

15/ 55

Composed applicatives are law-abiding

pure f ⊗ pure x
≡ (definition of ⊗ and pure)

F.pure (⊗G ) ⊗F F.pure (G.pure f) ⊗F F.pure (G.pure x)
≡ (homomorphism law for F (×2))

F.pure (G.pure f ⊗G G.pure x)
≡ (homomorphism law for G)

F.pure (G.pure (f x))

15/ 55

Composed applicatives are law-abiding

pure f ⊗ pure x
≡ (definition of ⊗ and pure)

F.pure (⊗G ) ⊗F F.pure (G.pure f) ⊗F F.pure (G.pure x)
≡ (homomorphism law for F (×2))

F.pure (G.pure f ⊗G G.pure x)
≡ (homomorphism law for G)

F.pure (G.pure (f x))
≡ (definition of pure)

pure (f x)

15/ 55

Fresh names, monadically

type ’a tree =

Empty : ’a tree

| Tree : ’a tree * ’a * ’a tree → ’a tree

module IState = State (struct type t = int end)

let fresh_name : string IState.t =

get >>= fun i →
put (i + 1) >>= fun () →
return (Printf.sprintf “x%d” i)

let rec label_tree : ’a tree → string tree IState.t =
function

Empty → return Empty
| Tree (l, v, r) →

label_tree l >>= fun l →
fresh_name >>= fun name →
label_tree r >>= fun r →
return (Tree (l, name , r))

16/ 55

Naming as a primitive effect

Problem: we cannot write fresh_name using the APPLICATIVE interface.

let fresh_name : string IState.t =

get >>= fun i →
put (i + 1) >>= fun () →
return (Printf.sprintf “x%d” i)

Solution: introduce fresh_name as a primitive effect:

implicit module NameA : sig

module Applicative : APPLICATIVE

val fresh_name : string Applicative.t

end = . . .

17/ 55

Traversing with namer

let rec label_tree : ’a tree → string tree NameA.t =
function

Empty → pure Empty
| Tree (l, v, r) →

pure (fun l name r → Tree (l, name , r))
⊗ label_tree l
⊗ fresh_name
⊗ label_tree r

18/ 55

The phantom monoid applicative

module type MONOID =

sig

type t

val zero : t

val (++) : t → t → t
end

module Phantom_monoid (M: MONOID)

: APPLICATIVE with type ’a t = M.t =

struct

type ’a t = M.t

let pure _ = M.zero

let (⊗) = M.(++)
end

19/ 55

The phantom monoid applicative

module type MONOID =

sig

type t

val zero : t

val (++) : t → t → t
end

module Phantom_monoid (M: MONOID)

: APPLICATIVE with type ’a t = M.t =

struct

type ’a t = M.t

let pure _ = M.zero

let (⊗) = M.(++)
end

Observation: we cannot implement Phantom_monoid as a monad.

19/ 55

Applicatives vs monads

programs


>>=

implementations

>>=

Some monadic programs are not applicative, e.g. fresh_name.

Some applicative instances are not monadic, e.g. Phantom_monoid.

20/ 55

Guideline: Postel’s law

Be conservative in what you do,
be liberal in what you accept from others.

21/ 55

Guideline: Postel’s law

Be conservative in what you do,
be liberal in what you accept from others.

Conservative in what you do: use applicatives, not monads.
(Applicatives give the implementor more freedom.)

21/ 55

Guideline: Postel’s law

Be conservative in what you do,
be liberal in what you accept from others.

Conservative in what you do: use applicatives, not monads.
(Applicatives give the implementor more freedom.)

Liberal in what you accept: implement monads, not applicatives.
(Monads give the user more power.)

21/ 55

Summary

monads

let x1 = e1 in

let x2 = e2 in

let xn = en in

e

applicatives

let x1 = e1
and x2 = e2

and xn = en in

e

22/ 55

Algebraic effects and handlers
(effect E)

23/ 55

Extending match for exceptions

Possible outcomes of match

match f v with

| A x → g x
| B y → h y
| . . .

f v evaluates to A x: evaluate g x

f v evaluates to B y: evaluate h y

. . .

E(

24/ 55

Extending match for exceptions

Possible outcomes of match

match f v with

| A x → g x
| B y → h y
| . . .

f v evaluates to A x: evaluate g x

f v evaluates to B y: evaluate h y

. . .

E(

24/ 55

Extending match for exceptions

Possible outcomes of match

match f v with

| A x → g x
| B y → h y
| . . .

f v evaluates to A x: evaluate g x

f v evaluates to B y: evaluate h y

. . .

E(

24/ 55

Extending match for exceptions

Possible outcomes of match

match f v with

| A x → g x
| B y → h y
| . . .

f v evaluates to A x: evaluate g x

f v evaluates to B y: evaluate h y

. . .

f v raises an exception E: raise E

24/ 55

Extending match for exceptions

Write:

match f v with

| A x → g x
| B y → h y
| . . .
| exception (E z) → j z

E.g. search an association list l (type (string * bool) list):

match List.assoc s l with

| true → “found (True)”
| false → “found (False)”
| exception Not_found → “not found”

25/ 55

Extending match for effects

Possible outcomes of match

match f v with

| A x → g x
| B y → h y
| exception (E z) → j z
| . . .

f v evaluates to A x: evaluate g x

f v evaluates to B y: evaluate h y

f v raises an exception E: raise E

. . .

f v performs an effect E and continues: perform E and continue

26/ 55

Extending match for effects

Possible outcomes of match

match f v with

| A x → g x
| B y → h y
| exception (E z) → j z
| . . .

f v evaluates to A x: evaluate g x

f v evaluates to B y: evaluate h y

f v raises an exception E: raise E

. . .

f v performs an effect E and continues: perform E and continue

26/ 55

Elements of exceptions

Exceptions

exception E: s → exn (means type exn += E: s → exn)

Raising exceptions

val raise : exn → ’b

Handling exceptions

match e with

. . .
| exception (E x) → . . .

Running continuations

continue : (’a, ’b) continuation → ’a → ’b

27/ 55

Elements of effects

Effects

effect E: s → t (means type _ eff += E: s → t eff)

Performing effects

val perform : ’a eff → ’a

Handling effects

match e with

. . .
| effect (E x) k → . . .

Running continuations

val continue : (’a, ’b) continuation → ’a → ’b

28/ 55

Using effects: yet another ocaml fork

modular implicits

opam switch 4.02.0+ modular -implicits

effects

opam remote add advanced -fp \

git:// github.com/ocamllabs/advanced -fp-repo

opam switch 4.03.0+ effects

staging (next week)

opam switch 4.02.1+ modular -implicits -ber

29/ 55

Example: exceptions as an effect
Define the effect and a function to perform the effect:

effect Raise : exn → ’a
let raise e = perform (Raise e)

Define a function to handle the effect:

let _try_ f handle =

match f () with

| v → v
| effect (Raise e) k → (* discard k! *) handle e

Program in direct (non-monadic) style:

let rec assoc x = function

| [] → raise Not_found
| (k,v)::t → if k = x then v else assoc x t

_try_ (fun () → Some (assoc 3 l))
(fun ex → None)

30/ 55

Recap: state as a monad
The type of computations:

type ’a t = state → state * ’a

The return and >>= functions from MONAD:

let return v s = (s, v)

let (>>=) m k s = let s’, a = m s in k a s’

Signatures of primitive effects:

val get : state t

val put : state → unit t

Primitive effects and a run function:

let get s = (s, s)

let put s’ _ = (s’, ())

let runState m init = m init

31/ 55

Example: state as an effect
Primitive effects:

effect Put : state → unit
effect Get : state

Functions to perform effects:

let put v = perform (Put v)

let get () = perform Get

A handler function:

let run f init =

let exec =

match f () with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s)

in exec init

32/ 55

Evaluating an effectful program

let run f init =

let exec =

match f () with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s)

in exec init

run (fun () →
let id = get () in

let () = put (id + 1) in

string_of_int id

) 3

33/ 55

Evaluating an effectful program

(match (fun () →
let id = get () in

let () = put (id + 1) in

string_of_int id) ()

with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s))
3

34/ 55

Evaluating an effectful program

(match (let id = get () in

let () = put (id + 1) in

string_of_int id)

with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s))
3

35/ 55

Evaluating an effectful program

(match (let id = perform Get in

let () = put (id + 1) in

string_of_int id)

with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s))
3

36/ 55

Evaluating an effectful program

(fun s → continue k s s) 3

37/ 55

Evaluating an effectful program

continue k 3 3

k =

(match (let id = – in

let () = put (id + 1) in

string_of_int id)

with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s))

38/ 55

Evaluating an effectful program

(match (let id = 3 in

let () = put (id + 1) in

string_of_int id)

with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s)) 3

39/ 55

Evaluating an effectful program

(match (let () = put (3 + 1) in

string_of_int 3)

with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s)) 3

40/ 55

Evaluating an effectful program

(match (let () = perform (Put 4) in

string_of_int 3)

with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s)) 3

41/ 55

Evaluating an effectful program

(fun s → continue k () 4) 3

k =

(match (let () = – in

string_of_int 3)

with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s))

42/ 55

Evaluating an effectful program

(match (let () = () in

string_of_int 3)

with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s))

4

43/ 55

Evaluating an effectful program

(match string_of_int 3

with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s))

4

44/ 55

Evaluating an effectful program

(match “3”

with

| x → (fun s → (s, x))
| effect (Put s’) k → (fun s → continue k () s’)
| effect Get k → (fun s → continue k s s))

4

45/ 55

Evaluating an effectful program

(fun s → (s, “3”)) 4

46/ 55

Evaluating an effectful program

(4, “3”)

47/ 55

Effects and monads

48/ 55

Integrating effects and monads

What we’ll get

Easy reuse of existing monadic code

(Uniformly turn monads into effects )

Improved efficiency, eliminating unnecessary binds

(Normalize computations before running them)

No need to write in monadic style

Use let instead of >>=

49/ 55

“Unnecessary” binds
The monad laws tell us that the following are equivalent:

return v >>= k ≡ k v
v >>= return ≡ v

Why would we ever write the lhs?

“Administrative” >>= and return arise through abstraction

let apply f x = f >>= fun g →
x >>= fun y →
return (g y)

. . .
apply (return succ) y

(* used: two returns , two >>=s *)
(* needed: one return , one >>= *)

50/ 55

Effects from monads: the elements

module type MONAD = sig

type +_ t

val return : ’a → ’a t
val bind : ’a t → (’a → ’b t) → ’b t

end

Given M : MONAD:

effect E : ’a M.t → ’a

let reify f = match f () with

| x → M.return x
| effect (E m) k → M.bind m (continue k)

let reflect m = perform (E m)

51/ 55

Effects from monads: the functor

module RR(M: MONAD) :

sig

val reify : (unit → ’a) → ’a M.t
val reflect : ’a M.t → ’a

end =

struct

effect E : ’a M.t → ’a

let reify f = match f () with

| x → M.return x
| effect (E m) k → M.bind m (continue k)

let reflect m = perform (E m)

end

52/ 55

Example: state effect from the state monad

module StateR = RR(State)

Build effectful functions from primitive effects get, put:

module StateR = RR(State)

let put v = StateR.reflect (State.put v)

let get () = StateR.reflect State.get

Build the handler from reify and State.run:

let run_state f init = State.run (StateR.reify f) init

Use let instead of >>=:

let id = get () in

let () = put (id + 1) in

string_of_int id

53/ 55

Summary

Applicatives are a weaker, more general interface to effects
(⊗ is less powerful than >>=)

Every applicative program can be written with monads
(but not vice versa)

Every Monad instance has a corresponding Applicative instance
(but not vice versa)

We can build effects using handlers

Existing monads transfer uniformly

54/ 55

Next time: multi-stage programming

.< e >.

55/ 55