git.iko.soy/Idris-dev
on 2b7db6a help sign in
Idris-dev/lib/Control/Monad/State.idr
29 lines 740 B history raw
1module Control.Monad.State
3import Control.Monad.Identity
4import Prelude.Monad
6%access public
8class Monad m => MonadState s (m : Set -> Set) where
9 get : m s
10 put : s -> m ()
12record StateT : Set -> (Set -> Set) -> Set -> Set where
13 ST : {m : Set -> Set} ->
14 (runStateT : s -> m (a, s)) -> StateT s m a
16instance Monad m => Monad (StateT s m) where
17 return x = ST (\st => return (x, st))
19 (ST f) >>= k = ST (\st => do (v, st') <- f st
20 let ST kv = k v
21 kv st')
23instance Monad m => MonadState s (StateT s m) where
24 get = ST (\x => return (x, x))
25 put x = ST (\y => return ((), x))
27State : Set -> Set -> Set
28State s a = StateT s Identity a