@@ -0,0 +1,29 @@
1+module control.monad.state
2+
3+import control.monad.identity
4+import prelude.monad
5+
6+%access public
7+
8+class Monad m => MonadState s (m : Set -> Set) where
9+ get : m s
10+ put : s -> m ()
11+
12+record StateT : Set -> (Set -> Set) -> Set -> Set where
13+ ST : {m : Set -> Set} ->
14+ (runStateT : s -> m (a, s)) -> StateT s m a
15+
16+instance Monad m => Monad (StateT s m) where
17+ return x = ST (\st => return (x, st))
18+
19+ (ST f) >>= k = ST (\st => do (v, st') <- f st
20+ let ST kv = k v
21+ kv st')
22+
23+instance Monad m => MonadState s (StateT s m) where
24+ get = ST (\x => return (x, x))
25+ put x = ST (\y => return ((), x))
26+
27+State : Set -> Set -> Set
28+State s a = StateT s Identity a
29+