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