git.iko.soy/Idris-dev
on master help sign in
Functor instance for StateT.
015200astartling
lib/Control/Monad/State.idr+6
compare with master
unifiedsplit
@@ -2,6 +2,7 @@ module Control.Monad.State
2
2
3import Control.Monad.Identity
3import Control.Monad.Identity
4import Prelude.Monad
4import Prelude.Monad
5+import Prelude.Functor
5
6
6%access public
7%access public
7
8
@@ -13,6 +14,11 @@ record StateT : Set -> (Set -> Set) -> Set -> Set where
13 ST : {m : Set -> Set} ->
14 ST : {m : Set -> Set} ->
14 (runStateT : s -> m (a, s)) -> StateT s m a
15 (runStateT : s -> m (a, s)) -> StateT s m a
15
16
17+instance 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)
21+
16instance Monad m => Monad (StateT s m) where
22instance Monad m => Monad (StateT s m) where
17 return x = ST (\st => return (x, st))
23 return x = ST (\st => return (x, st))
18
24