------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic definition and functions on the state monad transformer
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Effect.Monad.State.Transformer.Base where
open import Data.Product.Base using (_×_; proj₁; proj₂)
open import Data.Unit.Polymorphic.Base using (⊤)
open import Effect.Functor using (RawFunctor)
open import Function.Base using (_∘′_; const; id)
open import Level using (Level; suc; _⊔_)
private
variable
f s : Level
A : Set s
S : Set s
M : Set s → Set f
------------------------------------------------------------------------
-- State monad operations
record RawMonadState
(S : Set s)
(M : Set s → Set f)
: Set (suc s ⊔ f) where
field
gets : (S → A) → M A
modify : (S → S) → M ⊤
put = modify ∘′ const
get = gets id
------------------------------------------------------------------------
-- State monad transformer
record StateT
(S : Set s)
(M : Set s → Set f)
(A : Set s)
: Set (s ⊔ f) where
constructor mkStateT
field runStateT : S → M (S × A)
open StateT public
evalStateT : RawFunctor M → StateT S M A → S → M A
evalStateT M ma s = let open RawFunctor M in proj₂ <$> runStateT ma s
execStateT : RawFunctor M → StateT S M A → S → M S
execStateT M ma s = let open RawFunctor M in proj₁ <$> runStateT ma s
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