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