Last time: Overloading
val (=) : {E:EQ} → E.t → E.t → bool
1/ 52
This time: monads (etc.)
>>=
2/ 52
What do monads give us?
A general approach to implementing custom effects
A reusable interface to computation
A way to structure effectful programs in a functional language
3/ 52
Effects
4/ 52
What’s an effect?
An effect is anything a function does
besides mapping inputs to outputs.
If an expression M evaluates to a value V and changing
let x = M
in N
to
let x = V
in N
changes the behaviour then M also performs effects.
5/ 52
Example effects
Effects available in OCaml Effects unavailable in OCaml
(An effect is anything other than mapping inputs to outputs.)
6/ 52
Example effects
Effects available in OCaml
(higher-order) state
r := f; !r ()
Effects unavailable in OCaml
(An effect is anything other than mapping inputs to outputs.)
6/ 52
Example effects
Effects available in OCaml
(higher-order) state
r := f; !r ()
exceptions
raise Not_found
Effects unavailable in OCaml
(An effect is anything other than mapping inputs to outputs.)
6/ 52
Example effects
Effects available in OCaml
(higher-order) state
r := f; !r ()
exceptions
raise Not_found
I/O of various sorts
input_byte stdin
Effects unavailable in OCaml
(An effect is anything other than mapping inputs to outputs.)
6/ 52
Example effects
Effects available in OCaml
(higher-order) state
r := f; !r ()
exceptions
raise Not_found
I/O of various sorts
input_byte stdin
concurrency (interleaving)
Gc.finalise v f
Effects unavailable in OCaml
(An effect is anything other than mapping inputs to outputs.)
6/ 52
Example effects
Effects available in OCaml
(higher-order) state
r := f; !r ()
exceptions
raise Not_found
I/O of various sorts
input_byte stdin
concurrency (interleaving)
Gc.finalise v f
non-termination
let rec f x = f x
Effects unavailable in OCaml
(An effect is anything other than mapping inputs to outputs.)
6/ 52
Example effects
Effects available in OCaml
(higher-order) state
r := f; !r ()
exceptions
raise Not_found
I/O of various sorts
input_byte stdin
concurrency (interleaving)
Gc.finalise v f
non-termination
let rec f x = f x
Effects unavailable in OCaml
non-determinism
amb f g h
(An effect is anything other than mapping inputs to outputs.)
6/ 52
Example effects
Effects available in OCaml
(higher-order) state
r := f; !r ()
exceptions
raise Not_found
I/O of various sorts
input_byte stdin
concurrency (interleaving)
Gc.finalise v f
non-termination
let rec f x = f x
Effects unavailable in OCaml
non-determinism
amb f g h
first-class continuations
escape x in e
(An effect is anything other than mapping inputs to outputs.)
6/ 52
Example effects
Effects available in OCaml
(higher-order) state
r := f; !r ()
exceptions
raise Not_found
I/O of various sorts
input_byte stdin
concurrency (interleaving)
Gc.finalise v f
non-termination
let rec f x = f x
Effects unavailable in OCaml
non-determinism
amb f g h
first-class continuations
escape x in e
polymorphic state
r := “one”; r := 2
(An effect is anything other than mapping inputs to outputs.)
6/ 52
Example effects
Effects available in OCaml
(higher-order) state
r := f; !r ()
exceptions
raise Not_found
I/O of various sorts
input_byte stdin
concurrency (interleaving)
Gc.finalise v f
non-termination
let rec f x = f x
Effects unavailable in OCaml
non-determinism
amb f g h
first-class continuations
escape x in e
polymorphic state
r := “one”; r := 2
checked exceptions
int
IOError−−−−→ bool
(An effect is anything other than mapping inputs to outputs.)
6/ 52
Capturing effects in the types
Some languages capture effects in the type system.
We might have two function arrows:
a pure arrow a → b
an effectful arrow (or family of arrows) a⇝ b
and combinators for combining effectful functions
composeE : (a⇝ b) → (b ⇝ c) → (a⇝ c)
ignoreE : (a⇝ b) → (a⇝ unit)
pairE : (a⇝ b) → (c ⇝ d) → (a× c ⇝ b × d)
liftPure : (a → b) → (a⇝ b)
7/ 52
Separating application and performing effects
Alternative approach
Decompose effectful arrows into pure functions and computations
a⇝ b becomes a → T b
8/ 52
Monads
(let x = e in . . .)
9/ 52
Programming with monads
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)
10/ 52
Monads
module type MONAD = sig
type ’a t
val return : ’a → ’a t
val (>>=) : ’a t → (’a → ’b t) → ’b t
end
let return {M:MONAD} x = M.return x
let (>>=) {M:MONAD} m k = M.(>>=) m k
11/ 52
Monads
module type MONAD = sig
type ’a t
val return : ’a → ’a t
val (>>=) : ’a t → (’a → ’b t) → ’b t
end
let return {M:MONAD} x = M.return x
let (>>=) {M:MONAD} m k = M.(>>=) m k
Laws:
return v >>= k ≡ k v
v >>= return ≡ v
(m >>= f) >>= g ≡ m >>= (fun x → f x >>= g)
11/ 52
Monad laws: intuition
12/ 52
Monad laws: intuition
return v >>= k ≡ k v
let x = v in M ≡ M[x:=v]
12/ 52
Monad laws: intuition
return v >>= k ≡ k v
let x = v in M ≡ M[x:=v]
v >>= return ≡ v
let x = M in x ≡ M
12/ 52
Monad laws: intuition
return v >>= k ≡ k v
let x = v in M ≡ M[x:=v]
v >>= return ≡ v
let x = M in x ≡ M
(m >>= f) >>= g ≡ m >>= (fun x → f x >>= g)
let x = (let y = L in M)
in N
≡
let y = L in
let x = M in
N
12/ 52
Example: a state monad
module type STATE = sig
type state
type ’a t
module Monad : MONAD with type ’a t = ’a t
val get : state t
val put : state → unit t
val runState : ’a t → state → state * ’a
end
implicit module Monad_of_state{S:STATE} = S.Monad
13/ 52
Example: a state monad
module type STATE = sig
type state
type ’a t
module Monad : MONAD with type ’a t = ’a t
val get : state t
val put : state → unit t
val runState : ’a t → state → state * ’a
end
type ’a t = state → state * ’a
let return v s = (s, v)
14/ 52
Example: a state monad
module type STATE = sig
type state
type ’a t
module Monad : MONAD with type ’a t = ’a t
val get : state t
val put : state → unit t
val runState : ’a t → state → state * ’a
end
type ’a t = state → state * ’a
let (>>=) m k s = let s’, a = m s in k a s’
15/ 52
Example: a state monad
module type STATE = sig
type state
type ’a t
module Monad : MONAD with type ’a t = ’a t
val get : state t
val put : state → unit t
val runState : ’a t → state → state * ’a
end
type ’a t = state → state * ’a
let get s = (s, s)
16/ 52
Example: a state monad
module type STATE = sig
type state
type ’a t
module Monad : MONAD with type ’a t = ’a t
val get : state t
val put : state → unit t
val runState : ’a t → state → state * ’a
end
type ’a t = state → state * ’a
let put s’ _ = (s’, ())
17/ 52
Example: a state monad
module type STATE = sig
type state
type ’a t
module Monad : MONAD with type ’a t = ’a t
val get : state t
val put : state → unit t
val runState : ’a t → state → state * ’a
end
type ’a t = state → state * ’a
let runState m init = m init
18/ 52
Example: a state monad
module type STATE = sig
type state
type ’a t
module Monad : MONAD with type ’a t = ’a t
val get : state t
val put : state → unit t
val runState : ’a t → state → state * ’a
end
module State (S : sig type t end) = struct
type state = S.t
type ’a t = state -> state * ’a
module Monad = struct
type ’a t = state → state * ’a
let return v s = (s, v)
let (>>=) m k s = let s’, a = m s in k a s’
end
let get s = (s, s)
let put s’ _ = (s’, ())
let runState m init = m init
end
19/ 52
Example: a state monad
type ’a tree =
Empty : ’a tree
| Tree : ’a tree * ’a * ’a tree → ’a tree
implicit 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))
20/ 52
State satisfies the monad laws
return v >>= k
21/ 52
State satisfies the monad laws
return v >>= k
≡ (definition of return, >>=)
fun s → let s’, a = (fun s → (s, v)) s in k a s’
21/ 52
State satisfies the monad laws
return v >>= k
≡ (definition of return, >>=)
fun s → let s’, a = (fun s → (s, v)) s in k a s’
≡ (β)
fun s → let s’, a = (s, v) in k a s’
21/ 52
State satisfies the monad laws
return v >>= k
≡ (definition of return, >>=)
fun s → let s’, a = (fun s → (s, v)) s in k a s’
≡ (β)
fun s → let s’, a = (s, v) in k a s’
≡ (β for let)
fun s → k v s
21/ 52
State satisfies the monad laws
return v >>= k
≡ (definition of return, >>=)
fun s → let s’, a = (fun s → (s, v)) s in k a s’
≡ (β)
fun s → let s’, a = (s, v) in k a s’
≡ (β for let)
fun s → k v s
≡ (η)
k v
21/ 52
Example: exception
module type ERROR = sig
type error
type ’a t
module Monad : MONAD with type ’a t = ’a t
val raise : error → ’a t
val _try_ : ’a t → (error → ’a) → ’a
end
let rec find : ’a. (’a → bool) → ’a list → ’a t =
fun p l → match l with
[] → raise “Not found!”
| x :: _ when p x → return x
| _ :: xs → find p xs
_try_ (
find (greater 3) l >>= fun v →
return (string_of_int v)
)
(fun error → error)
22/ 52
Example: exception
module type ERROR = sig
type error
type ’a t
module Monad : MONAD with type ’a t = ’a t
val raise : error → ’a t
val _try_ : ’a t → (error → ’a) → ’a
end
type ’a t =
Val : ’a → ’a t
| Exn : error → ’a t
let return v = Val v
23/ 52
Example: exception
module type ERROR = sig
type error
type ’a t
module Monad : MONAD with type ’a t = ’a t
val raise : error → ’a t
val _try_ : ’a t → (error → ’a) → ’a
end
type ’a t =
Val : ’a → ’a t
| Exn : error → ’a t
let (>>=) m k = match m with
Val v → k v | Exn e → Exn e
24/ 52
Example: exception
module type ERROR = sig
type error
type ’a t
module Monad : MONAD with type ’a t = ’a t
val raise : error → ’a t
val _try_ : ’a t → (error → ’a) → ’a
end
type ’a t =
Val : ’a → ’a t
| Exn : error → ’a t
let raise e = Exn e
25/ 52
Example: exception
module type ERROR = sig
type error
type ’a t
module Monad : MONAD with type ’a t = ’a t
val raise : error → ’a t
val _try_ : ’a t → (error → ’a) → ’a
end
type ’a t =
Val : ’a → ’a t
| Exn : error → ’a t
let _try_ m catch = match m with
Val v → v | Exn e → catch e
26/ 52
Example: exception
module type ERROR = sig
type error
type ’a t
module Monad : MONAD with type ’a t = ’a t
val raise : error → ’a t
val _try_ : ’a t → (error → ’a) → ’a
end
module Error (E: sig type t end) = struct
type error = E.t
module Monad = struct
type ’a t =
Val : ’a → ’a t
| Exn : error → ’a t
let return v = Val v
let (>>=) m k = match m with
Val v → k v | Exn e → Exn e
end
let raise e = Exn e
let _try_ m catch = match m with
Val v → v | Exn e → catch e
end
27/ 52
Example: exception
let rec mapMTree : ’a. {M:MONAD} → (’a → ’b M.t) → ’
a tree → ’b tree M.t =
fun {M:MONAD} f l → match l with
Empty → return Empty
| Tree (l, v, r) →
mapMTree f l >>= fun l →
f v >>= fun v →
mapMTree f r >>= fun r →
return (Tree (l, v, r))
let check_nonzero =
mapMTree
(fun v →
if v = 0 then raise Zero
else return v)
28/ 52
Exception satisfies the monad laws
v >>= return
29/ 52
Exception satisfies the monad laws
v >>= return
≡ (definition of return, >>=)
match v with Val v → Val v | Exn e → Exn e
29/ 52
Exception satisfies the monad laws
v >>= return
≡ (definition of return, >>=)
match v with Val v → Val v | Exn e → Exn e
≡ (η for sums)
v
29/ 52
Higher-order
effectful programs
30/ 52
Monadic effects are higher-order
composeE : (a⇝ b) → (b ⇝ c) → (a⇝ c)
pairE : (a⇝ b) → (c ⇝ d) → (a× c ⇝ b × d)
uncurryE : (a⇝ b ⇝ c) → (a× b ⇝ c)
liftPure : (a → b) → (a⇝ b)
31/ 52
Higher-order computations with monads
val composeM : {M:MONAD} →
(’a → ’b M.t) → (’b → ’c M.t) → (’a → ’c M.t)
let composeM {M:MONAD} f g x : _ M.t =
f x >>= fun y →
g y
val uncurryM : {M:MONAD} →
(’a → (’b → ’c M.t) M.t) → ((’a * ’b) → ’c M.t)
let uncurryM {M:MONAD} f (x,y) : _ M.t =
f x >>= fun g →
g y
32/ 52
Applicatives
(let x = e . . . and)
33/ 52
Allowing only “static” effects
Idea: stop information flowing from one computation into another.
Only allow unparameterised computations:
1⇝ b
We can no longer write functions like this:
composeE : (a⇝ b) → (b ⇝ c) → (a⇝ c)
but some useful functions are still possible:
pairEstatic : (1⇝ a) → (1⇝ b) → (1⇝ a× b)
34/ 52
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
35/ 52