程序代写代做代考 Recap: effects

Recap: 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

1/ 26

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

2/ 26

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

3/ 26

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

4/ 26

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

5/ 26

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

6/ 26

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

7/ 26

Evaluating an effectful program

(fun s → continue k s s) 3

8/ 26

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))

9/ 26

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

10/ 26

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

11/ 26

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

12/ 26

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))

13/ 26

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

14/ 26

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

15/ 26

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

16/ 26

Evaluating an effectful program

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

17/ 26

Evaluating an effectful program

(4, “3”)

18/ 26

Effects and monads

19/ 26

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 >>=

20/ 26

“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 >>= *)

21/ 26

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)

22/ 26

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

23/ 26

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

24/ 26

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

25/ 26

Next time: multi-stage programming

.< e >.

26/ 26