程序代写代做代考 concurrency ocaml B tree Last time: Overloading

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