[state and identity monads ulfn@cs.chalmers.se**20071120204141] adddir ./Monad addfile ./Data/State.agda move ./Data/State.agda ./Monad/State.agda addfile ./Monad/Identity.agda hunk ./Monad/Identity.agda 1 + +module Monad.Identity where + +open import Monad + +Identity : Set -> Set +Identity A = A + +IdentityMonad : RawMonad Identity +IdentityMonad = record + { return = \x -> x + ; bind = \x f -> f x + } hunk ./Monad/State.agda 1 + +-- The state monad + +module Monad.State where + +open import Monad +open import Monad.Identity +open import Data.Product + +StateT : Set -> (Set -> Set) -> Set -> Set +StateT S M A = S -> M (A × S) + +StateTMonad : forall S {M} -> RawMonad M -> RawMonad (StateT S M) +StateTMonad s Mon = record + { return = \x s -> return (x , s) + ; bind = \m f s -> m s >>= \r -> f (proj₁ r) (proj₂ r) + } + where + open module M = MonadOps _ Mon + +StateTMonadZero : forall S {M} -> RawMonadZero M -> RawMonadZero (StateT S M) +StateTMonadZero S Mon = record + { monad = StateTMonad S (RawMonadZero.monad Mon) + ; mzero = \s -> mzero + } + where + open module M = MonadZeroOps _ Mon + +StateTMonadPlus : forall S {M} -> RawMonadPlus M -> RawMonadPlus (StateT S M) +StateTMonadPlus S Mon = record + { monadZero = StateTMonadZero S (RawMonadPlus.monadZero Mon) + ; plus = \m₁ m₂ s -> m₁ s ++ m₂ s + } + where + open module M = MonadPlusOps _ Mon + +State : Set -> Set -> Set +State S = StateT S Identity + +StateMonad : (S : Set) -> RawMonad (State S) +StateMonad S = StateTMonad S IdentityMonad