Monads.md (1495B)
1 +++ 2 title = 'Monads' 3 +++ 4 # Monads 5 ## Two operations, three laws 6 Monad: type constructor `m` that depends on type parameter `α`. 7 Has two operations: 8 - `pure {α : Type} : α → m α`: takes a type and wraps it in the monad 9 - `bind {α β : Type} : m α → (α → m β) → m β`: takes a type wrapped in monad, modifies it using a function, and returns it wrapped again 10 - `bind ma f` can also be written `ma >>= f` 11 12 In english, a monad is a box. `pure` puts stuff in the box, `bind` lets you use and modify stuff in the box. 13 14 The `←` operator inside `do` can extract stuff from the monad (take it out of the box). 15 16 First law: 17 18 ```lean 19 do 20 a' ← pure a, 21 f a' 22 = 23 f a 24 ``` 25 26 Second law: 27 28 ```lean 29 do 30 a ← ma, 31 pure a 32 = 33 ma 34 ``` 35 36 ## Mutable state 37 The state monad is based on an 'action': 38 39 ```lean 40 def action (σ α : Type) := 41 σ → α × σ 42 ``` 43 44 `σ` is the state here, or the 'context'. 45 46 Then you can have several operations on the state: 47 48 ```lean 49 def action.read {σ : Type} : action σ σ 50 | s := (s, s) 51 52 def action.write {σ : Type} (s : σ) : action σ unit 53 | _ := ((), s) 54 55 def action.pure {σ α : Type} (a : α) : action σ α 56 | s := (a, s) 57 58 def action.bind {σ : Type} {α β : Type} (ma : action σ α) (f : α → action σ β) : action σ β 59 | s := 60 match ma s with 61 | (a, s') := f a s' 62 end 63 ``` 64 65 ## Nondeterminism 66 When a program can return one of many possible values. 67 This can be modelled with sets -- i.e. it returns something from a set of values.