agda-stdlib/src/Effect/Monad/State/Transformer.agda at 7f5d072eb7f85351ddf43aa94deb8ee9fd21c890 · gallais/agda-stdlib · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
------------------------------------------------------------------------
-- The Agda standard library
--
-- The state monad transformer
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}


module Effect.Monad.State.Transformer where

open import Algebra using (RawMonoid)
open import Data.Product.Base using (_×_; _,_; map₂; proj₁; proj₂)
open import Data.Unit.Polymorphic.Base using (tt)
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus; RawMonadT; RawMonadTd)
open import Function.Base using (_∘′_; _$_; const)
open import Level using (Level; _⊔_)


private
  variable
    f s : Level
    A B : Set s
    S S₁ S₂ : Set s
    M : Set s → Set f

------------------------------------------------------------------------
-- Re-export the basic type and definitions

open import Effect.Monad.State.Transformer.Base public
  using ( RawMonadState
        ; StateT
        ; mkStateT
        ; runStateT
        ; evalStateT
        ; execStateT
        )

------------------------------------------------------------------------
-- Structure

functor : RawFunctor M → RawFunctor (StateT S M)
functor M = record
  { _<$>_ = λ f ma → mkStateT (λ s → map₂ f <$> StateT.runStateT ma s)
  } where open RawFunctor M

applicative : RawMonad M → RawApplicative (StateT S M)
applicative M = record
  { rawFunctor = functor rawFunctor
  ; pure = λ a → mkStateT (pure ∘′ (_, a))
  ; _<*>_ = λ mf mx → mkStateT $ λ s →
              do (s , f) ← StateT.runStateT mf s
                 (s , x) ← StateT.runStateT mx s
                 pure (s , f x)
  } where open RawMonad M

empty : RawEmpty M → RawEmpty (StateT S M)
empty M = record
  { empty = mkStateT (const (RawEmpty.empty M))
  }

choice : RawChoice M → RawChoice (StateT S M)
choice M = record
  { _<|>_ = λ ma₁ ma₂ → mkStateT $ λ s →
            StateT.runStateT ma₁ s
            <|> StateT.runStateT ma₂ s
  } where open RawChoice M

applicativeZero : RawMonadZero M → RawApplicativeZero (StateT S M)
applicativeZero M = record
  { rawApplicative = applicative (RawMonadZero.rawMonad M)
  ; rawEmpty = empty (RawMonadZero.rawEmpty M)
  }

alternative : RawMonadPlus M → RawAlternative (StateT S M)
alternative M = record
  { rawApplicativeZero = applicativeZero rawMonadZero
  ; rawChoice = choice rawChoice
  } where open RawMonadPlus M

monad : RawMonad M → RawMonad (StateT S M)
monad M = record
  { rawApplicative = applicative M
  ; _>>=_ = λ ma f → mkStateT $ λ s →
              do (s , a) ← StateT.runStateT ma s
                 StateT.runStateT (f a) s
  } where open RawMonad M

monadZero : RawMonadZero M → RawMonadZero (StateT S M)
monadZero M = record
  { rawMonad = monad (RawMonadZero.rawMonad M)
  ; rawEmpty = empty (RawMonadZero.rawEmpty M)
  }

monadPlus : RawMonadPlus M → RawMonadPlus (StateT S M)
monadPlus M = record
  { rawMonadZero = monadZero rawMonadZero
  ; rawChoice = choice rawChoice
  } where open RawMonadPlus M

------------------------------------------------------------------------
-- State monad transformer specifics

monadT : RawMonadT {f = s} {g₁ = f} {g₂ = s ⊔ f} (StateT S)
monadT M = record
  { lift = λ ma → mkStateT (λ s → (s ,_) <$> ma)
  ; rawMonad = monad M
  } where open RawMonad M

monadState : RawMonad M → RawMonadState S (StateT S M)
monadState M = record
  { gets   = λ f → mkStateT (λ s → pure (s , f s))
  ; modify = λ f → mkStateT (λ s → pure (f s , _))
  } where open RawMonad M

------------------------------------------------------------------------
-- State monad transformer specifics

liftStateT : RawMonad M →
             RawMonadState S₁ M →
             RawMonadState S₁ (StateT S₂ M)
liftStateT M Mon = record
  { gets   = λ f₁ → lift (gets f₁)
  ; modify = λ f₁ → lift (modify f₁)
  } where open RawMonadTd (monadT M) using (lift); open RawMonadState Mon

open import Effect.Monad.Reader.Transformer.Base

liftReaderT : RawMonadState S₁ M →
              RawMonadState S₁ (ReaderT S₂ M)
liftReaderT Mon = record
  { gets   = λ f → mkReaderT (const (gets f))
  ; modify = λ f → mkReaderT (const (modify f))
  } where open RawMonadState Mon

open import Effect.Monad.Writer.Transformer.Base

liftWriterT : (MS : RawMonoid s f) →
              RawFunctor M →
              RawMonadState S M →
              RawMonadState S (WriterT MS M)
liftWriterT MS M Mon = record
  { gets   = λ f → mkWriterT λ w → (gets ((w ,_) ∘′ f))
  ; modify = λ f → mkWriterT λ w → (const (w , tt) <$> modify f)
  } where open RawMonadState Mon
          open RawFunctor M