1
------------------------------------------------------------------------
3
------------------------------------------------------------------------
5
module Category.Monad.State where
7
open import Category.Monad
8
open import Category.Monad.Indexed
9
open import Category.Monad.Identity
10
open import Data.Product
11
open import Data.Function
13
open import Category.Applicative.Indexed
15
------------------------------------------------------------------------
16
-- Indexed state monads
18
IStateT : {I : Set} → (I → Set) → (Set → Set) → IFun I
19
IStateT S M i j A = S i → M (A × S j)
21
StateTIMonad : ∀ {I} (S : I → Set) {M} →
22
RawMonad M → RawIMonad (IStateT S M)
23
StateTIMonad S Mon = record
24
{ return = λ x s → return (x , s)
25
; _>>=_ = λ m f s → m s >>= uncurry f
27
where open RawMonad Mon
29
StateTIMonadZero : ∀ {I} (S : I → Set) {M} →
30
RawMonadZero M → RawIMonadZero (IStateT S M)
31
StateTIMonadZero S Mon = record
32
{ monad = StateTIMonad S (RawMonadZero.monad Mon)
35
where open RawMonadZero Mon
37
StateTIMonadPlus : ∀ {I} (S : I → Set) {M} →
38
RawMonadPlus M → RawIMonadPlus (IStateT S M)
39
StateTIMonadPlus S Mon = record
40
{ monadZero = StateTIMonadZero S (RawIMonadPlus.monadZero Mon)
41
; _∣_ = λ m₁ m₂ s → m₁ s ∣ m₂ s
43
where open RawMonadPlus Mon
45
------------------------------------------------------------------------
46
-- State monad operations
48
record RawIMonadState {I : Set} (S : I → Set)
49
(M : I → I → Set → Set) : Set₁ where
52
get : ∀ {i} → M i i (S i)
53
put : ∀ {i j} → S j → M i j ⊤
55
open RawIMonad monad public
57
modify : ∀ {i j} → (S i → S j) → M i j ⊤
58
modify f = get >>= put ∘ f
60
StateTIMonadState : ∀ {I} (S : I → Set) {M} →
61
RawMonad M → RawIMonadState S (IStateT S M)
62
StateTIMonadState S Mon = record
63
{ monad = StateTIMonad S Mon
64
; get = λ s → return (s , s)
65
; put = λ s _ → return (_ , s)
67
where open RawIMonad Mon
69
------------------------------------------------------------------------
70
-- Ordinary state monads
72
RawMonadState : Set → (Set → Set) → Set₁
73
RawMonadState S M = RawIMonadState {⊤} (λ _ → S) (λ _ _ → M)
75
module RawMonadState {S : Set} {M : Set → Set}
76
(Mon : RawMonadState S M) where
77
open RawIMonadState Mon public
79
StateT : Set → (Set → Set) → Set → Set
80
StateT S M = IStateT {⊤} (λ _ → S) M _ _
82
StateTMonad : ∀ S {M} → RawMonad M → RawMonad (StateT S M)
83
StateTMonad S = StateTIMonad (λ _ → S)
85
StateTMonadZero : ∀ S {M} → RawMonadZero M → RawMonadZero (StateT S M)
86
StateTMonadZero S = StateTIMonadZero (λ _ → S)
88
StateTMonadPlus : ∀ S {M} → RawMonadPlus M → RawMonadPlus (StateT S M)
89
StateTMonadPlus S = StateTIMonadPlus (λ _ → S)
91
StateTMonadState : ∀ S {M} → RawMonad M → RawMonadState S (StateT S M)
92
StateTMonadState S = StateTIMonadState (λ _ → S)
94
State : Set → Set → Set
95
State S = StateT S Identity
97
StateMonad : (S : Set) → RawMonad (State S)
98
StateMonad S = StateTMonad S IdentityMonad
100
StateMonadState : ∀ S → RawMonadState S (State S)
101
StateMonadState S = StateTMonadState S IdentityMonad
103
LiftMonadState : ∀ {S₁} S₂ {M} →
105
RawMonadState S₁ (StateT S₂ M)
106
LiftMonadState S₂ Mon = record
107
{ monad = StateTIMonad (λ _ → S₂) monad
108
; get = λ s → get >>= λ x → return (x , s)
109
; put = λ s′ s → put s′ >> return (_ , s)
111
where open RawIMonadState Mon
added
removed
src/Category/Monad/State.agda
