git.iko.soy/Idris-dev
on b4d856a help sign in
Idris-dev/lib/Control/Monad/State.idr
42 lines 1.2 kB history raw
1module Control.Monad.State
3import Control.Monad.Identity
4import Prelude.Monad
5import Prelude.Functor
7%access public
9class Monad m => MonadState s (m : Type -> Type) where
10 get : m s
11 put : s -> m ()
13record StateT : Type -> (Type -> Type) -> Type -> Type where
14 ST : {m : Type -> Type} ->
15 (runStateT : s -> m (a, s)) -> StateT s m a
17instance Functor f => Functor (StateT s f) where
18 fmap f (ST g) = ST (\st => fmap (mapFst f) (g st)) where
19 mapFst : (a -> x) -> (a, b) -> (x, b)
20 mapFst fn (a, b) = (fn a, b)
22instance Monad f => Applicative (StateT s f) where
23 pure x = ST (\st => pure (x, st))
25 (ST f) <$> (ST a) = ST (\st => do (g, r) <- f st
26 (b, t) <- a r
27 return (g b, t))
29instance Monad m => Monad (StateT s m) where
30 return x = ST (\st => return (x, st))
32 (ST f) >>= k = ST (\st => do (v, st') <- f st
33 let ST kv = k v
34 kv st')
36instance Monad m => MonadState s (StateT s m) where
37 get = ST (\x => return (x, x))
38 put x = ST (\y => return ((), x))
40State : Type -> Type -> Type
41State s a = StateT s Identity a