------------------------------------------------------------------------
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4