0 | module Control.Monad.State.Interface
 1 |
 2 | import Control.Monad.Maybe
 3 | import Control.Monad.Error.Either
 4 | import Control.Monad.Reader.Reader
 5 | import Control.Monad.State.State
 6 | import Control.Monad.RWS.CPS
 7 | import Control.Monad.Trans
 8 | import Control.Monad.Writer.CPS
 9 |
10 | %default total
11 |
12 | ||| A monadic computation that has access to state.
13 | public export
14 | interface Monad m => MonadState stateType m | m where
15 |     ||| Get the context
16 |     get : m stateType
17 |     ||| Write a new context/output
18 |     put : stateType -> m ()
19 |
20 |     ||| Embed a simple state action into the monad.
21 |     state : (stateType -> (stateType,a)) -> m a
22 |     state f = do s <- get
23 |                  let (s2,a) = f s
24 |                  put s2
25 |                  pure a
26 |
27 | ||| Apply a function to modify the context of this computation
28 | public export
29 | modify : MonadState stateType m => (stateType -> stateType) -> m ()
30 | modify f
31 |     = do s <- get
32 |          put (f s)
33 |
34 | ||| Evaluate a function in the context held by this computation
35 | public export
36 | gets : MonadState stateType m => (stateType -> a) -> m a
37 | gets f
38 |     = do s <- get
39 |          pure (f s)
40 |
41 | --------------------------------------------------------------------------------
42 | --          Implementations
43 | --------------------------------------------------------------------------------
44 |
45 | public export %inline
46 | Monad m => MonadState stateType (StateT stateType m) where
47 |     get     = ST (\x => pure (x, x))
48 |     put x   = ST (\y => pure (x, ()))
49 |     state f = ST $ pure . f
50 |
51 | public export %inline
52 | MonadState s m => MonadState s (EitherT e m) where
53 |   get = lift get
54 |   put = lift . put
55 |   state = lift . state
56 |
57 | public export %inline
58 | MonadState s m => MonadState s (MaybeT m) where
59 |   get = lift get
60 |   put = lift . put
61 |   state = lift . state
62 |
63 | public export %inline
64 | Monad m => MonadState s (RWST r w s m) where
65 |   get     = MkRWST $ \_,s,w => pure (s,s,w)
66 |   put s   = MkRWST $ \_,_,w => pure ((),s,w)
67 |   state f = MkRWST $ \_,s,w => let (s',a) = f s in pure (a,s',w)
68 |
69 | public export %inline
70 | MonadState s m => MonadState s (ReaderT r m) where
71 |   get = lift get
72 |   put = lift . put
73 |   state = lift . state
74 |
75 | public export %inline
76 | MonadState s m => MonadState s (WriterT r m) where
77 |   get = lift get
78 |   put = lift . put
79 |   state = lift . state
80 |