git.iko.soy/Idris-dev
on 4e34dfd help sign in
Idris-dev/libs/base/Control/Monad/State.idr
57 lines 1.8 kB history raw
1module Control.Monad.State
3import Control.Monad.Identity
4import Control.Monad.Trans
6%access public
8||| A computation which runs in a context and produces an output
9class Monad m => MonadState s (m : Type -> Type) | m where
10 ||| Get the context
11 get : m s
12 ||| Write a new context/output
13 put : s -> m ()
15||| The transformer on which the State monad is based
16record StateT : Type -> (Type -> Type) -> Type -> Type where
17 ST : {m : Type -> Type} ->
18 (runStateT : s -> m (a, s)) -> StateT s m a
20instance Functor f => Functor (StateT s f) where
21 map f (ST g) = ST (\st => map (mapFst f) (g st)) where
22 mapFst : (a -> x) -> (a, s) -> (x, s)
23 mapFst fn (a, b) = (fn a, b)
25instance Monad f => Applicative (StateT s f) where
26 pure x = ST (\st => pure (x, st))
28 (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st
29 (b, t) <- a r
30 return (g b, t))
32instance Monad m => Monad (StateT s m) where
33 (ST f) >>= k = ST (\st => do (v, st') <- f st
34 let ST kv = k v
35 kv st')
37instance Monad m => MonadState s (StateT s m) where
38 get = ST (\x => return (x, x))
39 put x = ST (\y => return ((), x))
41instance MonadTrans (StateT s) where
42 lift x = ST (\st => do r <- x
43 return (r, st))
45||| Apply a function to modify the context of this computation
46modify : MonadState s m => (s -> s) -> m ()
47modify f = do s <- get
48 put (f s)
50||| Evaluate a function in the context held by this computation
51gets : MonadState s m => (s -> a) -> m a
52gets f = do s <- get
53 return (f s)
55||| The State monad. See the MonadState class
56State : Type -> Type -> Type
57State s a = StateT s Identity a