mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-11 02:01:36 +03:00
Merge pull request #960 from stefan-hoeck/transformer-overhaul
This commit is contained in:
G. Allais
GitHub
commit
af94feb18e
@ -1,156 +1,4 @@
|
||||
module Control.Monad.Either
|
||||
|
||||
-------------------------------------------------
|
||||
-- The monad transformer `EitherT e m a` equips a monad with the ability to
|
||||
-- return a choice of two values.
|
||||
|
||||
-- Sequenced actions of `Either e m a` produce a value `a` only if none of the
|
||||
-- actions in the sequence returned `e`. Because returning `e` exits the
|
||||
-- computation early, this can be seen as equipping a monad with the ability to
|
||||
-- throw an exception.
|
||||
|
||||
-- This is more powerful than MaybeT which instead equips a monad with the
|
||||
-- ability to not return a result.
|
||||
-------------------------------------------------
|
||||
|
||||
import Control.Monad.Trans
|
||||
import Control.Monad.Reader
|
||||
import Control.Monad.State
|
||||
|
||||
public export
|
||||
data EitherT : (e : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
|
||||
MkEitherT : m (Either e a) -> EitherT e m a
|
||||
|
||||
export
|
||||
%inline
|
||||
runEitherT : EitherT e m a -> m (Either e a)
|
||||
runEitherT (MkEitherT x) = x
|
||||
|
||||
export
|
||||
eitherT : Monad m => (a -> m c) -> (b -> m c) -> EitherT a m b -> m c
|
||||
eitherT f g x = runEitherT x >>= either f g
|
||||
|
||||
||| map the underlying computation
|
||||
||| The basic 'unwrap, apply, rewrap' of this transformer.
|
||||
export
|
||||
%inline
|
||||
mapEitherT : (m (Either e a) -> n (Either e' a')) -> EitherT e m a -> EitherT e' n a'
|
||||
mapEitherT f = MkEitherT . f . runEitherT
|
||||
|
||||
export
|
||||
bimapEitherT : Functor m => (a -> c) -> (b -> d)
|
||||
-> EitherT a m b -> EitherT c m d
|
||||
bimapEitherT f g x = mapEitherT (map (either (Left . f) (Right . g))) x
|
||||
|
||||
||| Analogous to Left, aka throwE
|
||||
export
|
||||
%inline
|
||||
left : Applicative m => e -> EitherT e m a
|
||||
left = MkEitherT . pure . Left
|
||||
|
||||
||| Analogous to Right, aka pure for EitherT
|
||||
export
|
||||
%inline
|
||||
right : Applicative m => a -> EitherT e m a
|
||||
right = MkEitherT . pure . Right
|
||||
|
||||
export
|
||||
swapEitherT : Functor m => EitherT e m a -> EitherT a m e
|
||||
swapEitherT = mapEitherT (map (either Right Left))
|
||||
|
||||
-------------------------------------------------
|
||||
-- Methods of the 'exception' theme
|
||||
-------------------------------------------------
|
||||
|
||||
||| aka `left`
|
||||
export
|
||||
%inline
|
||||
throwE : Applicative m => e -> EitherT e m a
|
||||
throwE = MkEitherT . pure . Left
|
||||
|
||||
export
|
||||
catchE : Monad m => EitherT e m a -> (e -> EitherT e' m a) -> EitherT e' m a
|
||||
catchE et f
|
||||
= MkEitherT $ runEitherT et >>= either (runEitherT . f) (pure . Right)
|
||||
|
||||
|
||||
-------------------------------------------------
|
||||
-- Interface Implementations
|
||||
-------------------------------------------------
|
||||
|
||||
public export
|
||||
Eq (m (Either e a)) => Eq (EitherT e m a) where
|
||||
(==) = (==) `on` runEitherT
|
||||
|
||||
public export
|
||||
Ord (m (Either e a)) => Ord (EitherT e m a) where
|
||||
compare = compare `on` runEitherT
|
||||
|
||||
public export
|
||||
Show (m (Either e a)) => Show (EitherT e m a) where
|
||||
showPrec d (MkEitherT x) = showCon d "MkEitherT" $ showArg x
|
||||
|
||||
-- I'm not actually confident about having this instance but it is a sane
|
||||
-- default and since idris has named implementations it can be swapped out at
|
||||
-- the use site.
|
||||
public export
|
||||
Monad m => Semigroup (EitherT e m a) where
|
||||
MkEitherT x <+> MkEitherT y = MkEitherT $ do
|
||||
r@(Right _) <- x
|
||||
| Left _ => y
|
||||
pure r
|
||||
|
||||
public export
|
||||
Functor m => Functor (EitherT e m) where
|
||||
map f e = MkEitherT $ map f <$> runEitherT e
|
||||
|
||||
public export
|
||||
Foldable m => Foldable (EitherT e m) where
|
||||
foldr f acc (MkEitherT e)
|
||||
= foldr (\x,xs => either (const xs) (`f` xs) x) acc e
|
||||
|
||||
null (MkEitherT e) = null e
|
||||
|
||||
public export
|
||||
Traversable m => Traversable (EitherT e m) where
|
||||
traverse f (MkEitherT x)
|
||||
= MkEitherT <$> traverse (either (pure . Left) (map Right . f)) x
|
||||
|
||||
public export
|
||||
Applicative m => Applicative (EitherT e m) where
|
||||
pure = MkEitherT . pure . Right
|
||||
f <*> x = MkEitherT [| runEitherT f <*> runEitherT x |]
|
||||
|
||||
public export
|
||||
Monad m => Monad (EitherT e m) where
|
||||
x >>= k = MkEitherT $ runEitherT x >>= either (pure . Left) (runEitherT . k)
|
||||
|
||||
||| Alternative instance that collects left results, allowing you to try
|
||||
||| multiple possibilities and combine failures.
|
||||
public export
|
||||
(Monad m, Monoid e) => Alternative (EitherT e m) where
|
||||
empty = left neutral
|
||||
MkEitherT x <|> MkEitherT y = MkEitherT $ do
|
||||
Left l <- x
|
||||
| Right r => pure (Right r)
|
||||
Left l' <- y
|
||||
| Right r => pure (Right r)
|
||||
pure (Left (l <+> l'))
|
||||
|
||||
public export
|
||||
MonadTrans (EitherT e) where
|
||||
lift = MkEitherT . map Right
|
||||
|
||||
public export
|
||||
HasIO m => HasIO (EitherT e m) where
|
||||
liftIO act = MkEitherT $ liftIO (io_bind act (pure . Right))
|
||||
|
||||
public export
|
||||
MonadReader r m => MonadReader r (EitherT e m) where
|
||||
ask = lift ask
|
||||
local f (MkEitherT x) = MkEitherT (local f x)
|
||||
|
||||
public export
|
||||
MonadState s m => MonadState s (EitherT e m) where
|
||||
get = lift get
|
||||
put = lift . put
|
||||
import public Control.Monad.Error.Either as Control.Monad.Either
|
||||
import public Control.Monad.Error.Interface as Control.Monad.Either
|
||||
|
||||
144
libs/base/Control/Monad/Error/Either.idr
Normal file
144
libs/base/Control/Monad/Error/Either.idr
Normal file
@ -0,0 +1,144 @@
|
||||
module Control.Monad.Error.Either
|
||||
|
||||
-------------------------------------------------
|
||||
-- The monad transformer `EitherT e m a` equips a monad with the ability to
|
||||
-- return a choice of two values.
|
||||
|
||||
-- Sequenced actions of `Either e m a` produce a value `a` only if none of the
|
||||
-- actions in the sequence returned `e`. Because returning `e` exits the
|
||||
-- computation early, this can be seen as equipping a monad with the ability to
|
||||
-- throw an exception.
|
||||
|
||||
-- This is more powerful than MaybeT which instead equips a monad with the
|
||||
-- ability to not return a result.
|
||||
-------------------------------------------------
|
||||
|
||||
import Control.Monad.Trans
|
||||
|
||||
public export
|
||||
data EitherT : (e : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
|
||||
MkEitherT : m (Either e a) -> EitherT e m a
|
||||
|
||||
public export
|
||||
%inline
|
||||
runEitherT : EitherT e m a -> m (Either e a)
|
||||
runEitherT (MkEitherT x) = x
|
||||
|
||||
public export
|
||||
eitherT : Monad m => (a -> m c) -> (b -> m c) -> EitherT a m b -> m c
|
||||
eitherT f g x = runEitherT x >>= either f g
|
||||
|
||||
||| map the underlying computation
|
||||
||| The basic 'unwrap, apply, rewrap' of this transformer.
|
||||
public export
|
||||
%inline
|
||||
mapEitherT : (m (Either e a) -> n (Either e' a')) -> EitherT e m a -> EitherT e' n a'
|
||||
mapEitherT f = MkEitherT . f . runEitherT
|
||||
|
||||
public export
|
||||
bimapEitherT : Functor m => (a -> c) -> (b -> d)
|
||||
-> EitherT a m b -> EitherT c m d
|
||||
bimapEitherT f g x = mapEitherT (map (either (Left . f) (Right . g))) x
|
||||
|
||||
||| Analogous to Left, aka throwE
|
||||
public export
|
||||
%inline
|
||||
left : Applicative m => e -> EitherT e m a
|
||||
left = MkEitherT . pure . Left
|
||||
|
||||
||| Analogous to Right, aka pure for EitherT
|
||||
public export
|
||||
%inline
|
||||
right : Applicative m => a -> EitherT e m a
|
||||
right = MkEitherT . pure . Right
|
||||
|
||||
public export
|
||||
swapEitherT : Functor m => EitherT e m a -> EitherT a m e
|
||||
swapEitherT = mapEitherT (map (either Right Left))
|
||||
|
||||
-------------------------------------------------
|
||||
-- Methods of the 'exception' theme
|
||||
-------------------------------------------------
|
||||
|
||||
||| aka `left`
|
||||
public export
|
||||
%inline
|
||||
throwE : Applicative m => e -> EitherT e m a
|
||||
throwE = MkEitherT . pure . Left
|
||||
|
||||
public export
|
||||
catchE : Monad m => EitherT e m a -> (e -> EitherT e' m a) -> EitherT e' m a
|
||||
catchE et f
|
||||
= MkEitherT $ runEitherT et >>= either (runEitherT . f) (pure . Right)
|
||||
|
||||
|
||||
-------------------------------------------------
|
||||
-- Interface Implementations
|
||||
-------------------------------------------------
|
||||
|
||||
public export
|
||||
Eq (m (Either e a)) => Eq (EitherT e m a) where
|
||||
(==) = (==) `on` runEitherT
|
||||
|
||||
public export
|
||||
Ord (m (Either e a)) => Ord (EitherT e m a) where
|
||||
compare = compare `on` runEitherT
|
||||
|
||||
public export
|
||||
Show (m (Either e a)) => Show (EitherT e m a) where
|
||||
showPrec d (MkEitherT x) = showCon d "MkEitherT" $ showArg x
|
||||
|
||||
-- I'm not actually confident about having this instance but it is a sane
|
||||
-- default and since idris has named implementations it can be swapped out at
|
||||
-- the use site.
|
||||
public export
|
||||
Monad m => Semigroup (EitherT e m a) where
|
||||
MkEitherT x <+> MkEitherT y = MkEitherT $ do
|
||||
r@(Right _) <- x
|
||||
| Left _ => y
|
||||
pure r
|
||||
|
||||
public export
|
||||
Functor m => Functor (EitherT e m) where
|
||||
map f e = MkEitherT $ map f <$> runEitherT e
|
||||
|
||||
public export
|
||||
Foldable m => Foldable (EitherT e m) where
|
||||
foldr f acc (MkEitherT e)
|
||||
= foldr (\x,xs => either (const xs) (`f` xs) x) acc e
|
||||
|
||||
null (MkEitherT e) = null e
|
||||
|
||||
public export
|
||||
Traversable m => Traversable (EitherT e m) where
|
||||
traverse f (MkEitherT x)
|
||||
= MkEitherT <$> traverse (either (pure . Left) (map Right . f)) x
|
||||
|
||||
public export
|
||||
Applicative m => Applicative (EitherT e m) where
|
||||
pure = MkEitherT . pure . Right
|
||||
f <*> x = MkEitherT [| runEitherT f <*> runEitherT x |]
|
||||
|
||||
public export
|
||||
Monad m => Monad (EitherT e m) where
|
||||
x >>= k = MkEitherT $ runEitherT x >>= either (pure . Left) (runEitherT . k)
|
||||
|
||||
||| Alternative instance that collects left results, allowing you to try
|
||||
||| multiple possibilities and combine failures.
|
||||
public export
|
||||
(Monad m, Monoid e) => Alternative (EitherT e m) where
|
||||
empty = left neutral
|
||||
MkEitherT x <|> MkEitherT y = MkEitherT $ do
|
||||
Left l <- x
|
||||
| Right r => pure (Right r)
|
||||
Left l' <- y
|
||||
| Right r => pure (Right r)
|
||||
pure (Left (l <+> l'))
|
||||
|
||||
public export
|
||||
MonadTrans (EitherT e) where
|
||||
lift = MkEitherT . map Right
|
||||
|
||||
public export
|
||||
HasIO m => HasIO (EitherT e m) where
|
||||
liftIO act = MkEitherT $ liftIO (io_bind act (pure . Right))
|
||||
113
libs/base/Control/Monad/Error/Interface.idr
Normal file
113
libs/base/Control/Monad/Error/Interface.idr
Normal file
@ -0,0 +1,113 @@
|
||||
||| The Error monad (also called the Exception monad).
|
||||
module Control.Monad.Error.Interface
|
||||
|
||||
import Control.Monad.Error.Either
|
||||
import Control.Monad.Maybe
|
||||
import Control.Monad.RWS.CPS
|
||||
import Control.Monad.Reader.Reader
|
||||
import Control.Monad.State.State
|
||||
import Control.Monad.Trans
|
||||
import Control.Monad.Writer.CPS
|
||||
|
||||
||| The strategy of combining computations that can throw exceptions
|
||||
||| by bypassing bound functions
|
||||
||| from the point an exception is thrown to the point that it is handled.
|
||||
||| Is parameterized over the type of error information and
|
||||
||| the monad type constructor.
|
||||
||| It is common to use `Either String` as the monad type constructor
|
||||
||| for an error monad in which error descriptions take the form of strings.
|
||||
||| In that case and many other common cases the resulting monad is already defined
|
||||
||| as an instance of the 'MonadError' class.
|
||||
public export
|
||||
interface Monad m => MonadError e m | m where
|
||||
||| Is used within a monadic computation to begin exception processing.
|
||||
throwError : e -> m a
|
||||
|
||||
||| A handler function to handle previous errors and return to normal execution.
|
||||
||| A common idiom is:
|
||||
|||
|
||||
||| ```idris example
|
||||
||| do { action1; action2; action3 } `catchError` handler
|
||||
||| ```
|
||||
catchError : m a -> (e -> m a) -> m a
|
||||
|
||||
||| Lifts an `Either e` into any `MonadError e`.
|
||||
public export
|
||||
liftEither : MonadError e m => Either e a -> m a
|
||||
liftEither = either throwError pure
|
||||
|
||||
||| Makes a success or failure of an action visible in
|
||||
||| the return type.
|
||||
public export
|
||||
tryError : MonadError e m => m a -> m (Either e a)
|
||||
tryError action = (map Right action) `catchError` (pure . Left)
|
||||
|
||||
||| `MonadError` analogue to the `withEitherT` function.
|
||||
||| Modify the value (but not the type) of an error.
|
||||
||| If you need to change the type of `e` use `mapError`.
|
||||
public export
|
||||
withError : MonadError e m => (e -> e) -> m a -> m a
|
||||
withError f action = tryError action >>= either (throwError . f) pure
|
||||
|
||||
||| Flipped version of `catchError`.
|
||||
public export
|
||||
handleError : MonadError e m => (e -> m a) -> m a -> m a
|
||||
handleError = flip catchError
|
||||
|
||||
||| `MonadError` analogue of the `mapEitherT` function. The
|
||||
||| computation is unwrapped, a function is applied to the `Either`, and
|
||||
||| the result is lifted into the second `MonadError` instance.
|
||||
public export
|
||||
mapError : (MonadError e m, MonadError e' n)
|
||||
=> (m (Either e a) -> n (Either e' b)) -> m a -> n b
|
||||
mapError f action = f (tryError action) >>= liftEither
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Implementations
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export
|
||||
MonadError () Maybe where
|
||||
throwError () = Nothing
|
||||
catchError Nothing f = f ()
|
||||
catchError x _ = x
|
||||
|
||||
public export
|
||||
MonadError e (Either e) where
|
||||
throwError = Left
|
||||
Left l `catchError` h = h l
|
||||
Right r `catchError` _ = Right r
|
||||
|
||||
public export
|
||||
Monad m => MonadError e (EitherT e m) where
|
||||
throwError = throwE
|
||||
catchError = catchE
|
||||
|
||||
public export
|
||||
MonadError e m => MonadError e (MaybeT m) where
|
||||
throwError = lift . throwError
|
||||
catchError (MkMaybeT m) f = MkMaybeT (catchError m (runMaybeT . f))
|
||||
|
||||
public export
|
||||
MonadError e m => MonadError e (ReaderT r m) where
|
||||
throwError = lift . throwError
|
||||
catchError (MkReaderT m) f =
|
||||
MkReaderT \e => catchError (m e) (runReaderT e . f)
|
||||
|
||||
public export
|
||||
MonadError e m => MonadError e (StateT r m) where
|
||||
throwError = lift . throwError
|
||||
catchError (ST m) f =
|
||||
ST \s => catchError (m s) (runStateT s . f)
|
||||
|
||||
public export
|
||||
MonadError e m => MonadError e (RWST r w s m) where
|
||||
throwError = lift . throwError
|
||||
catchError (MkRWST m) f =
|
||||
MkRWST \r,w,s => catchError (m r w s) (\e => unRWST (f e) r w s)
|
||||
|
||||
public export
|
||||
MonadError e m => MonadError e (WriterT w m) where
|
||||
throwError = lift . throwError
|
||||
catchError (MkWriterT m) f =
|
||||
MkWriterT \w => catchError (m w) (\e => unWriterT (f e) w)
|
||||
@ -12,59 +12,57 @@ module Control.Monad.Maybe
|
||||
-------------------------------------------------
|
||||
|
||||
import Control.Monad.Trans
|
||||
import Control.Monad.Reader
|
||||
import Control.Monad.State
|
||||
import Data.Maybe
|
||||
|
||||
public export
|
||||
data MaybeT : (m : Type -> Type) -> (a : Type) -> Type where
|
||||
MkMaybeT : m (Maybe a) -> MaybeT m a
|
||||
|
||||
export
|
||||
public export
|
||||
%inline
|
||||
runMaybeT : MaybeT m a -> m (Maybe a)
|
||||
runMaybeT (MkMaybeT x) = x
|
||||
|
||||
export
|
||||
public export
|
||||
%inline
|
||||
isNothingT : Functor m => MaybeT m a -> m Bool
|
||||
isNothingT = map isNothing . runMaybeT
|
||||
|
||||
export
|
||||
public export
|
||||
%inline
|
||||
isJustT : Functor m => MaybeT m a -> m Bool
|
||||
isJustT = map isJust . runMaybeT
|
||||
|
||||
export
|
||||
public export
|
||||
%inline
|
||||
maybeT : Monad m => m b -> (a -> m b) -> MaybeT m a -> m b
|
||||
maybeT v g x = runMaybeT x >>= maybe v g
|
||||
|
||||
export
|
||||
public export
|
||||
%inline
|
||||
fromMaybeT : Monad m => m a -> MaybeT m a -> m a
|
||||
fromMaybeT v x = runMaybeT x >>= maybe v pure
|
||||
|
||||
export
|
||||
public export
|
||||
%inline
|
||||
toMaybeT : Functor m => Bool -> m a -> MaybeT m a
|
||||
toMaybeT b m = MkMaybeT $ map (\a => toMaybe b a) m
|
||||
|
||||
||| map the underlying computation
|
||||
||| The basic 'unwrap, apply, rewrap' of this transformer.
|
||||
export
|
||||
public export
|
||||
%inline
|
||||
mapMaybeT : (m (Maybe a) -> n (Maybe a')) -> MaybeT m a -> MaybeT n a'
|
||||
mapMaybeT f = MkMaybeT . f . runMaybeT
|
||||
|
||||
||| Analogous to Just, aka pure for MaybeT
|
||||
export
|
||||
public export
|
||||
%inline
|
||||
just : Applicative m => a -> MaybeT m a
|
||||
just = MkMaybeT . pure . Just
|
||||
|
||||
||| Analogous to Nothing, aka empty for MaybeT
|
||||
export
|
||||
public export
|
||||
%inline
|
||||
nothing : Applicative m => MaybeT m a
|
||||
nothing = MkMaybeT $ pure Nothing
|
||||
@ -139,13 +137,3 @@ MonadTrans MaybeT where
|
||||
public export
|
||||
HasIO m => HasIO (MaybeT m) where
|
||||
liftIO act = MkMaybeT $ liftIO (io_bind act (pure . Just))
|
||||
|
||||
public export
|
||||
MonadReader r m => MonadReader r (MaybeT m) where
|
||||
ask = lift ask
|
||||
local f (MkMaybeT x) = MkMaybeT (local f x)
|
||||
|
||||
public export
|
||||
MonadState s m => MonadState s (MaybeT m) where
|
||||
get = lift get
|
||||
put = lift . put
|
||||
|
||||
7
libs/base/Control/Monad/RWS.idr
Normal file
7
libs/base/Control/Monad/RWS.idr
Normal file
@ -0,0 +1,7 @@
|
||||
module Control.Monad.RWS
|
||||
|
||||
import public Control.Monad.RWS.CPS as Control.Monad.RWS
|
||||
import public Control.Monad.RWS.Interface as Control.Monad.RWS
|
||||
import public Control.Monad.Reader.Interface as Control.Monad.RWS
|
||||
import public Control.Monad.Writer.Interface as Control.Monad.RWS
|
||||
import public Control.Monad.State.Interface as Control.Monad.RWS
|
||||
133
libs/base/Control/Monad/RWS/CPS.idr
Normal file
133
libs/base/Control/Monad/RWS/CPS.idr
Normal file
@ -0,0 +1,133 @@
|
||||
||| Note: The difference to a 'strict' RWST implementation is
|
||||
||| that accumulation of values does not happen in the
|
||||
||| Applicative and Monad instances but when invoking `Writer`-specific
|
||||
||| functions like `writer` or `listen`.
|
||||
module Control.Monad.RWS.CPS
|
||||
|
||||
import Control.Monad.Identity
|
||||
import Control.Monad.Trans
|
||||
|
||||
||| A monad transformer adding reading an environment of type `r`,
|
||||
||| collecting an output of type `w` and updating a state of type `s`
|
||||
||| to an inner monad `m`.
|
||||
public export
|
||||
record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
|
||||
constructor MkRWST
|
||||
unRWST : r -> s -> w -> m (a, s, w)
|
||||
|
||||
||| Unwrap an RWST computation as a function. (The inverse of `rwsT`.)
|
||||
public export %inline
|
||||
runRWST : Monoid w => RWST r w s m a -> r -> s -> m (a, s, w)
|
||||
runRWST m r s = unRWST m r s neutral
|
||||
|
||||
||| Construct an RWST computation from a function. (The inverse of `runRWST`.)
|
||||
public export %inline
|
||||
rwsT : (Functor m, Semigroup w) => (r -> s -> m (a, s, w)) -> RWST r w s m a
|
||||
rwsT f = MkRWST $ \r,s,w => (\(a,s',w') => (a,s',w <+> w')) <$> f r s
|
||||
|
||||
||| Evaluate a computation with the given initial state and environment,
|
||||
||| returning the final value and output, discarding the final state.
|
||||
public export %inline
|
||||
evalRWST : (Functor m, Monoid w) => RWST r w s m a -> r -> s -> m (a,w)
|
||||
evalRWST m r s = (\(a,_,w) => (a,w)) <$> runRWST m r s
|
||||
|
||||
||| Evaluate a computation with the given initial state and environment,
|
||||
||| returning the final state and output, discarding the final value.
|
||||
public export %inline
|
||||
execRWST : (Functor m, Monoid w) => RWST r w s m a -> r -> s -> m (s,w)
|
||||
execRWST m r s = (\(_,s',w) => (s',w)) <$> runRWST m r s
|
||||
|
||||
||| Map the inner computation using the given function.
|
||||
public export %inline
|
||||
mapRWST : (Functor n, Monoid w, Semigroup w')
|
||||
=> (m (a, s, w) -> n (b, s, w')) -> RWST r w s m a -> RWST r w' s n b
|
||||
mapRWST f m = MkRWST \r,s,w =>
|
||||
(\(a,s',w') => (a,s',w <+> w')) <$> f (runRWST m r s)
|
||||
|
||||
||| `withRWST f m` executes action `m` with an initial environment
|
||||
||| and state modified by applying `f`.
|
||||
public export %inline
|
||||
withRWST : (r' -> s -> (r, s)) -> RWST r w s m a -> RWST r' w s m a
|
||||
withRWST f m = MkRWST \r,s => uncurry (unRWST m) (f r s)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- RWS Functions
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| A monad containing an environment of type `r`, output of type `w`
|
||||
||| and an updatable state of type `s`.
|
||||
public export
|
||||
RWS : (r : Type) -> (w : Type) -> (s : Type) -> (a : Type) -> Type
|
||||
RWS r w s = RWST r w s Identity
|
||||
|
||||
||| Unwrap an RWS computation as a function. (The inverse of `rws`.)
|
||||
public export %inline
|
||||
runRWS : Monoid w => RWS r w s a -> r -> s -> (a, s, w)
|
||||
runRWS m r s = runIdentity (runRWST m r s)
|
||||
|
||||
||| Construct an RWS computation from a function. (The inverse of `runRWS`.)
|
||||
public export %inline
|
||||
rws : Semigroup w => (r -> s -> (a, s, w)) -> RWS r w s a
|
||||
rws f = MkRWST \r,s,w => let (a, s', w') = f r s
|
||||
in Id (a, s', w <+> w')
|
||||
|
||||
||| Evaluate a computation with the given initial state and environment,
|
||||
||| returning the final value and output, discarding the final state.
|
||||
public export %inline
|
||||
evalRWS : Monoid w => RWS r w s a -> r -> s -> (a,w)
|
||||
evalRWS m r s = let (a,_,w) = runRWS m r s
|
||||
in (a,w)
|
||||
|
||||
||| Evaluate a computation with the given initial state and environment,
|
||||
||| returning the final state and output, discarding the final value.
|
||||
public export %inline
|
||||
execRWS : Monoid w => RWS r w s a -> r -> s -> (s,w)
|
||||
execRWS m r s = let (_,s1,w) = runRWS m r s
|
||||
in (s1,w)
|
||||
|
||||
||| Map the return value, final state and output of a computation using
|
||||
||| the given function.
|
||||
public export %inline
|
||||
mapRWS : (Monoid w, Semigroup w')
|
||||
=> ((a, s, w) -> (b, s, w')) -> RWS r w s a -> RWS r w' s b
|
||||
mapRWS f = mapRWST \(Id p) => Id (f p)
|
||||
|
||||
||| `withRWS f m` executes action `m` with an initial environment
|
||||
||| and state modified by applying `f`.
|
||||
public export %inline
|
||||
withRWS : (r' -> s -> (r, s)) -> RWS r w s a -> RWS r' w s a
|
||||
withRWS = withRWST
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Implementations
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export %inline
|
||||
Functor m => Functor (RWST r w s m) where
|
||||
map f m = MkRWST \r,s,w => (\(a,s',w') => (f a,s',w')) <$> unRWST m r s w
|
||||
|
||||
public export %inline
|
||||
Monad m => Applicative (RWST r w s m) where
|
||||
pure a = MkRWST \_,s,w => pure (a,s,w)
|
||||
MkRWST mf <*> MkRWST mx =
|
||||
MkRWST \r,s,w => do (f,s1,w1) <- mf r s w
|
||||
(a,s2,w2) <- mx r s1 w1
|
||||
pure (f a,s2,w2)
|
||||
|
||||
public export %inline
|
||||
(Monad m, Alternative m) => Alternative (RWST r w s m) where
|
||||
empty = MkRWST \_,_,_ => empty
|
||||
MkRWST m <|> MkRWST n = MkRWST \r,s,w => m r s w <|> n r s w
|
||||
|
||||
public export %inline
|
||||
Monad m => Monad (RWST r w s m) where
|
||||
m >>= k = MkRWST \r,s,w => do (a,s1,w1) <- unRWST m r s w
|
||||
unRWST (k a) r s1 w1
|
||||
|
||||
public export %inline
|
||||
MonadTrans (RWST r w s) where
|
||||
lift m = MkRWST \_,s,w => map (\a => (a,s,w)) m
|
||||
|
||||
public export %inline
|
||||
HasIO m => HasIO (RWST r w s m) where
|
||||
liftIO = lift . liftIO
|
||||
13
libs/base/Control/Monad/RWS/Interface.idr
Normal file
13
libs/base/Control/Monad/RWS/Interface.idr
Normal file
@ -0,0 +1,13 @@
|
||||
module Control.Monad.RWS.Interface
|
||||
|
||||
import Control.Monad.RWS.CPS
|
||||
import Control.Monad.Reader.Interface
|
||||
import Control.Monad.State.Interface
|
||||
import Control.Monad.Writer.Interface
|
||||
|
||||
public export
|
||||
interface (MonadReader r m, MonadWriter w m, MonadState s m) =>
|
||||
MonadRWS r w s m | m where
|
||||
|
||||
public export
|
||||
(Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where
|
||||
@ -1,81 +1,4 @@
|
||||
module Control.Monad.Reader
|
||||
|
||||
import Control.Monad.Identity
|
||||
import Control.Monad.Trans
|
||||
|
||||
||| A computation which runs in a static context and produces an output
|
||||
public export
|
||||
interface Monad m => MonadReader stateType m | m where
|
||||
||| Get the context
|
||||
ask : m stateType
|
||||
|
||||
||| `local f c` runs the computation `c` in an environment modified by `f`.
|
||||
local : MonadReader stateType m => (stateType -> stateType) -> m a -> m a
|
||||
|
||||
||| The transformer on which the Reader monad is based
|
||||
public export
|
||||
record ReaderT (stateType : Type) (m : Type -> Type) (a : Type) where
|
||||
constructor MkReaderT
|
||||
1 runReaderT' : stateType -> m a
|
||||
|
||||
public export
|
||||
implementation Functor f => Functor (ReaderT stateType f) where
|
||||
map f (MkReaderT g) = MkReaderT (\st => map f (g st))
|
||||
|
||||
public export
|
||||
implementation Applicative f => Applicative (ReaderT stateType f) where
|
||||
pure x = MkReaderT (\st => pure x)
|
||||
|
||||
(MkReaderT f) <*> (MkReaderT a) =
|
||||
MkReaderT (\st =>
|
||||
let f' = f st in
|
||||
let a' = a st in
|
||||
f' <*> a')
|
||||
|
||||
public export
|
||||
implementation Monad m => Monad (ReaderT stateType m) where
|
||||
(MkReaderT f) >>= k =
|
||||
MkReaderT (\st => do v <- f st
|
||||
let MkReaderT kv = k v
|
||||
kv st)
|
||||
|
||||
public export
|
||||
implementation MonadTrans (ReaderT stateType) where
|
||||
lift x = MkReaderT (\_ => x)
|
||||
|
||||
public export
|
||||
implementation Monad m => MonadReader stateType (ReaderT stateType m) where
|
||||
ask = MkReaderT (\st => pure st)
|
||||
|
||||
local f (MkReaderT action) = MkReaderT (action . f)
|
||||
|
||||
public export
|
||||
implementation HasIO m => HasIO (ReaderT stateType m) where
|
||||
liftIO f = MkReaderT (\_ => liftIO f)
|
||||
|
||||
public export
|
||||
implementation (Monad f, Alternative f) => Alternative (ReaderT stateType f) where
|
||||
empty = lift empty
|
||||
|
||||
(MkReaderT f) <|> (MkReaderT g) = MkReaderT (\st => f st <|> g st)
|
||||
|
||||
||| Evaluate a function in the context held by this computation
|
||||
public export
|
||||
asks : MonadReader stateType m => (stateType -> a) -> m a
|
||||
asks f = ask >>= pure . f
|
||||
|
||||
||| Unwrap and apply a ReaderT monad computation
|
||||
public export
|
||||
%inline
|
||||
runReaderT : stateType -> ReaderT stateType m a -> m a
|
||||
runReaderT s action = runReaderT' action s
|
||||
|
||||
||| The Reader monad. The ReaderT transformer applied to the Identity monad.
|
||||
public export
|
||||
Reader : (stateType : Type) -> (a : Type) -> Type
|
||||
Reader s a = ReaderT s Identity a
|
||||
|
||||
||| Unwrap and apply a Reader monad computation
|
||||
public export
|
||||
runReader : stateType -> Reader stateType a -> a
|
||||
runReader s = runIdentity . runReaderT s
|
||||
import public Control.Monad.Reader.Reader as Control.Monad.Reader
|
||||
import public Control.Monad.Reader.Interface as Control.Monad.Reader
|
||||
|
||||
65
libs/base/Control/Monad/Reader/Interface.idr
Normal file
65
libs/base/Control/Monad/Reader/Interface.idr
Normal file
@ -0,0 +1,65 @@
|
||||
module Control.Monad.Reader.Interface
|
||||
|
||||
import Control.Monad.Maybe
|
||||
import Control.Monad.Error.Either
|
||||
import Control.Monad.Reader.Reader
|
||||
import Control.Monad.State.State
|
||||
import Control.Monad.RWS.CPS
|
||||
import Control.Monad.Trans
|
||||
import Control.Monad.Writer.CPS
|
||||
|
||||
||| A computation which runs in a static context and produces an output
|
||||
public export
|
||||
interface Monad m => MonadReader stateType m | m where
|
||||
||| Get the context
|
||||
ask : m stateType
|
||||
|
||||
||| `local f c` runs the computation `c` in an environment modified by `f`.
|
||||
local : MonadReader stateType m => (stateType -> stateType) -> m a -> m a
|
||||
|
||||
|
||||
||| Evaluate a function in the context held by this computation
|
||||
public export
|
||||
asks : MonadReader stateType m => (stateType -> a) -> m a
|
||||
asks f = map f ask
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Implementations
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export %inline
|
||||
Monad m => MonadReader stateType (ReaderT stateType m) where
|
||||
ask = MkReaderT (\st => pure st)
|
||||
|
||||
local f (MkReaderT action) = MkReaderT (action . f)
|
||||
|
||||
public export %inline
|
||||
Monad m => MonadReader r (RWST r w s m) where
|
||||
ask = MkRWST \r,s,w => pure (r,s,w)
|
||||
local f m = MkRWST \r,s,w => unRWST m (f r) s w
|
||||
|
||||
public export %inline
|
||||
MonadReader r m => MonadReader r (EitherT e m) where
|
||||
ask = lift ask
|
||||
local = mapEitherT . local
|
||||
|
||||
public export %inline
|
||||
MonadReader r m => MonadReader r (MaybeT m) where
|
||||
ask = lift ask
|
||||
local = mapMaybeT . local
|
||||
|
||||
public export %inline
|
||||
MonadReader r m => MonadReader r (StateT s m) where
|
||||
ask = lift ask
|
||||
local = mapStateT . local
|
||||
|
||||
public export %inline
|
||||
MonadReader r m => MonadReader r (WriterT w m) where
|
||||
ask = lift ask
|
||||
|
||||
-- this differs from the implementation in the mtl package
|
||||
-- which uses mapWriterT. However, it seems strange that
|
||||
-- this should require a Monoid instance to further
|
||||
-- accumulate values, while the implementation of
|
||||
-- MonadReader for RWST does no such thing.
|
||||
local f (MkWriterT m) = MkWriterT \w => local f (m w)
|
||||
74
libs/base/Control/Monad/Reader/Reader.idr
Normal file
74
libs/base/Control/Monad/Reader/Reader.idr
Normal file
@ -0,0 +1,74 @@
|
||||
module Control.Monad.Reader.Reader
|
||||
|
||||
import Control.Monad.Identity
|
||||
import Control.Monad.Trans
|
||||
|
||||
||| The transformer on which the Reader monad is based
|
||||
public export
|
||||
record ReaderT (stateType : Type) (m : Type -> Type) (a : Type) where
|
||||
constructor MkReaderT
|
||||
1 runReaderT' : stateType -> m a
|
||||
|
||||
||| Transform the computation inside a @ReaderT@.
|
||||
public export %inline
|
||||
mapReaderT : (m a -> n b) -> ReaderT r m a -> ReaderT r n b
|
||||
mapReaderT f m = MkReaderT \st => f (runReaderT' m st)
|
||||
|
||||
||| Unwrap and apply a ReaderT monad computation
|
||||
public export
|
||||
%inline
|
||||
runReaderT : stateType -> ReaderT stateType m a -> m a
|
||||
runReaderT s action = runReaderT' action s
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Reader
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| The Reader monad. The ReaderT transformer applied to the Identity monad.
|
||||
public export
|
||||
Reader : (stateType : Type) -> (a : Type) -> Type
|
||||
Reader s a = ReaderT s Identity a
|
||||
|
||||
||| Unwrap and apply a Reader monad computation
|
||||
public export %inline
|
||||
runReader : stateType -> Reader stateType a -> a
|
||||
runReader s = runIdentity . runReaderT s
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Implementations
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export
|
||||
implementation Functor f => Functor (ReaderT stateType f) where
|
||||
map f (MkReaderT g) = MkReaderT (\st => map f (g st))
|
||||
|
||||
public export
|
||||
implementation Applicative f => Applicative (ReaderT stateType f) where
|
||||
pure x = MkReaderT (\st => pure x)
|
||||
|
||||
(MkReaderT f) <*> (MkReaderT a) =
|
||||
MkReaderT (\st =>
|
||||
let f' = f st in
|
||||
let a' = a st in
|
||||
f' <*> a')
|
||||
|
||||
public export
|
||||
implementation Monad m => Monad (ReaderT stateType m) where
|
||||
(MkReaderT f) >>= k =
|
||||
MkReaderT (\st => do v <- f st
|
||||
let MkReaderT kv = k v
|
||||
kv st)
|
||||
|
||||
public export
|
||||
implementation MonadTrans (ReaderT stateType) where
|
||||
lift x = MkReaderT (\_ => x)
|
||||
|
||||
public export
|
||||
implementation HasIO m => HasIO (ReaderT stateType m) where
|
||||
liftIO f = MkReaderT (\_ => liftIO f)
|
||||
|
||||
public export
|
||||
implementation (Monad f, Alternative f) => Alternative (ReaderT stateType f) where
|
||||
empty = lift empty
|
||||
|
||||
(MkReaderT f) <|> (MkReaderT g) = MkReaderT (\st => f st <|> g st)
|
||||
@ -1,111 +1,6 @@
|
||||
module Control.Monad.State
|
||||
|
||||
import public Control.Monad.Identity
|
||||
import public Control.Monad.Trans
|
||||
|
||||
||| A computation which runs in a context and produces an output
|
||||
public export
|
||||
interface Monad m => MonadState stateType m | m where
|
||||
||| Get the context
|
||||
get : m stateType
|
||||
||| Write a new context/output
|
||||
put : stateType -> m ()
|
||||
|
||||
||| The transformer on which the State monad is based
|
||||
public export
|
||||
record StateT (stateType : Type) (m : Type -> Type) (a : Type) where
|
||||
constructor ST
|
||||
runStateT' : stateType -> m (stateType, a)
|
||||
|
||||
public export
|
||||
implementation Functor f => Functor (StateT stateType f) where
|
||||
map f (ST g) = ST (\st => map (map f) (g st)) where
|
||||
|
||||
public export
|
||||
implementation Monad f => Applicative (StateT stateType f) where
|
||||
pure x = ST (\st => pure (st, x))
|
||||
|
||||
(ST f) <*> (ST a)
|
||||
= ST (\st =>
|
||||
do (r, g) <- f st
|
||||
(t, b) <- a r
|
||||
pure (t, g b))
|
||||
|
||||
public export
|
||||
implementation Monad m => Monad (StateT stateType m) where
|
||||
(ST f) >>= k
|
||||
= ST (\st =>
|
||||
do (st', v) <- f st
|
||||
let ST kv = k v
|
||||
kv st')
|
||||
|
||||
public export
|
||||
implementation Monad m => MonadState stateType (StateT stateType m) where
|
||||
get = ST (\x => pure (x, x))
|
||||
put x = ST (\y => pure (x, ()))
|
||||
|
||||
public export
|
||||
implementation MonadTrans (StateT stateType) where
|
||||
lift x
|
||||
= ST (\st =>
|
||||
do r <- x
|
||||
pure (st, r))
|
||||
|
||||
public export
|
||||
implementation (Monad f, Alternative f) => Alternative (StateT st f) where
|
||||
empty = lift empty
|
||||
(ST f) <|> (ST g) = ST (\st => f st <|> g st)
|
||||
|
||||
public export
|
||||
implementation HasIO m => HasIO (StateT stateType m) where
|
||||
liftIO io = ST $ \s => liftIO $ io_bind io $ \a => pure (s, a)
|
||||
|
||||
||| Apply a function to modify the context of this computation
|
||||
public export
|
||||
modify : MonadState stateType m => (stateType -> stateType) -> m ()
|
||||
modify f
|
||||
= do s <- get
|
||||
put (f s)
|
||||
|
||||
||| Evaluate a function in the context held by this computation
|
||||
public export
|
||||
gets : MonadState stateType m => (stateType -> a) -> m a
|
||||
gets f
|
||||
= do s <- get
|
||||
pure (f s)
|
||||
|
||||
||| Unwrap and apply a StateT monad computation.
|
||||
public export
|
||||
%inline
|
||||
runStateT : stateType -> StateT stateType m a -> m (stateType, a)
|
||||
runStateT s act = runStateT' act s
|
||||
|
||||
||| Unwrap and apply a StateT monad computation, but discard the final state.
|
||||
public export
|
||||
evalStateT : Functor m => stateType -> StateT stateType m a -> m a
|
||||
evalStateT s = map snd . runStateT s
|
||||
|
||||
||| Unwrap and apply a StateT monad computation, but discard the resulting value.
|
||||
public export
|
||||
execStateT : Functor m => stateType -> StateT stateType m a -> m stateType
|
||||
execStateT s = map fst . runStateT s
|
||||
|
||||
||| The State monad. See the MonadState interface
|
||||
public export
|
||||
State : (stateType : Type) -> (ty : Type) -> Type
|
||||
State = \s, a => StateT s Identity a
|
||||
|
||||
||| Unwrap and apply a State monad computation.
|
||||
public export
|
||||
runState : stateType -> State stateType a -> (stateType, a)
|
||||
runState s act = runIdentity (runStateT s act)
|
||||
|
||||
||| Unwrap and apply a State monad computation, but discard the final state.
|
||||
public export
|
||||
evalState : stateType -> State stateType a -> a
|
||||
evalState s = snd . runState s
|
||||
|
||||
||| Unwrap and apply a State monad computation, but discard the resulting value.
|
||||
public export
|
||||
execState : stateType -> State stateType a -> stateType
|
||||
execState s = fst . runState s
|
||||
import public Control.Monad.Identity -- left here for compatibility
|
||||
import public Control.Monad.Trans -- left here for compatibility
|
||||
import public Control.Monad.State.Interface as Control.Monad.State
|
||||
import public Control.Monad.State.State as Control.Monad.State
|
||||
|
||||
78
libs/base/Control/Monad/State/Interface.idr
Normal file
78
libs/base/Control/Monad/State/Interface.idr
Normal file
@ -0,0 +1,78 @@
|
||||
module Control.Monad.State.Interface
|
||||
|
||||
import Control.Monad.Maybe
|
||||
import Control.Monad.Error.Either
|
||||
import Control.Monad.Reader.Reader
|
||||
import Control.Monad.State.State
|
||||
import Control.Monad.RWS.CPS
|
||||
import Control.Monad.Trans
|
||||
import Control.Monad.Writer.CPS
|
||||
|
||||
||| A computation which runs in a context and produces an output
|
||||
public export
|
||||
interface Monad m => MonadState stateType m | m where
|
||||
||| Get the context
|
||||
get : m stateType
|
||||
||| Write a new context/output
|
||||
put : stateType -> m ()
|
||||
|
||||
||| Embed a simple state action into the monad.
|
||||
state : (stateType -> (stateType,a)) -> m a
|
||||
state f = do s <- get
|
||||
let (s2,a) = f s
|
||||
put s2
|
||||
pure a
|
||||
|
||||
||| Apply a function to modify the context of this computation
|
||||
public export
|
||||
modify : MonadState stateType m => (stateType -> stateType) -> m ()
|
||||
modify f
|
||||
= do s <- get
|
||||
put (f s)
|
||||
|
||||
||| Evaluate a function in the context held by this computation
|
||||
public export
|
||||
gets : MonadState stateType m => (stateType -> a) -> m a
|
||||
gets f
|
||||
= do s <- get
|
||||
pure (f s)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Implementations
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export %inline
|
||||
Monad m => MonadState stateType (StateT stateType m) where
|
||||
get = ST (\x => pure (x, x))
|
||||
put x = ST (\y => pure (x, ()))
|
||||
state f = ST $ pure . f
|
||||
|
||||
public export %inline
|
||||
MonadState s m => MonadState s (EitherT e m) where
|
||||
get = lift get
|
||||
put = lift . put
|
||||
state = lift . state
|
||||
|
||||
public export %inline
|
||||
MonadState s m => MonadState s (MaybeT m) where
|
||||
get = lift get
|
||||
put = lift . put
|
||||
state = lift . state
|
||||
|
||||
public export %inline
|
||||
Monad m => MonadState s (RWST r w s m) where
|
||||
get = MkRWST \_,s,w => pure (s,s,w)
|
||||
put s = MkRWST \_,_,w => pure ((),s,w)
|
||||
state f = MkRWST \_,s,w => let (s',a) = f s in pure (a,s',w)
|
||||
|
||||
public export %inline
|
||||
MonadState s m => MonadState s (ReaderT r m) where
|
||||
get = lift get
|
||||
put = lift . put
|
||||
state = lift . state
|
||||
|
||||
public export %inline
|
||||
MonadState s m => MonadState s (WriterT r m) where
|
||||
get = lift get
|
||||
put = lift . put
|
||||
state = lift . state
|
||||
104
libs/base/Control/Monad/State/State.idr
Normal file
104
libs/base/Control/Monad/State/State.idr
Normal file
@ -0,0 +1,104 @@
|
||||
module Control.Monad.State.State
|
||||
|
||||
import Control.Monad.Identity
|
||||
import Control.Monad.Trans
|
||||
|
||||
||| The transformer on which the State monad is based
|
||||
public export
|
||||
record StateT (stateType : Type) (m : Type -> Type) (a : Type) where
|
||||
constructor ST
|
||||
runStateT' : stateType -> m (stateType, a)
|
||||
|
||||
||| Unwrap and apply a StateT monad computation.
|
||||
public export
|
||||
%inline
|
||||
runStateT : stateType -> StateT stateType m a -> m (stateType, a)
|
||||
runStateT s act = runStateT' act s
|
||||
|
||||
||| Unwrap and apply a StateT monad computation, but discard the final state.
|
||||
public export %inline
|
||||
evalStateT : Functor m => stateType -> StateT stateType m a -> m a
|
||||
evalStateT s = map snd . runStateT s
|
||||
|
||||
||| Unwrap and apply a StateT monad computation, but discard the resulting value.
|
||||
public export %inline
|
||||
execStateT : Functor m => stateType -> StateT stateType m a -> m stateType
|
||||
execStateT s = map fst . runStateT s
|
||||
|
||||
||| Map both the return value and final state of a computation using
|
||||
||| the given function.
|
||||
public export %inline
|
||||
mapStateT : (m (s, a) -> n (s, b)) -> StateT s m a -> StateT s n b
|
||||
mapStateT f m = ST $ f . runStateT' m
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- State
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| The State monad. See the MonadState interface
|
||||
public export
|
||||
State : (stateType : Type) -> (ty : Type) -> Type
|
||||
State = \s, a => StateT s Identity a
|
||||
|
||||
||| Unwrap and apply a State monad computation.
|
||||
public export %inline
|
||||
runState : stateType -> State stateType a -> (stateType, a)
|
||||
runState s act = runIdentity (runStateT s act)
|
||||
|
||||
||| Unwrap and apply a State monad computation, but discard the final state.
|
||||
public export %inline
|
||||
evalState : stateType -> State stateType a -> a
|
||||
evalState s = snd . runState s
|
||||
|
||||
||| Unwrap and apply a State monad computation, but discard the resulting value.
|
||||
public export %inline
|
||||
execState : stateType -> State stateType a -> stateType
|
||||
execState s = fst . runState s
|
||||
|
||||
||| Map both the return value and final state of a computation using
|
||||
||| the given function.
|
||||
public export %inline
|
||||
mapState : ((s, a) -> (s, b)) -> State s a -> State s b
|
||||
mapState f = mapStateT \(Id p) => Id (f p)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Implementations
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export
|
||||
implementation Functor f => Functor (StateT stateType f) where
|
||||
map f (ST g) = ST (\st => map (map f) (g st)) where
|
||||
|
||||
public export
|
||||
implementation Monad f => Applicative (StateT stateType f) where
|
||||
pure x = ST (\st => pure (st, x))
|
||||
|
||||
(ST f) <*> (ST a)
|
||||
= ST (\st =>
|
||||
do (r, g) <- f st
|
||||
(t, b) <- a r
|
||||
pure (t, g b))
|
||||
|
||||
public export
|
||||
implementation Monad m => Monad (StateT stateType m) where
|
||||
(ST f) >>= k
|
||||
= ST (\st =>
|
||||
do (st', v) <- f st
|
||||
let ST kv = k v
|
||||
kv st')
|
||||
|
||||
public export
|
||||
implementation MonadTrans (StateT stateType) where
|
||||
lift x
|
||||
= ST (\st =>
|
||||
do r <- x
|
||||
pure (st, r))
|
||||
|
||||
public export
|
||||
implementation (Monad f, Alternative f) => Alternative (StateT st f) where
|
||||
empty = lift empty
|
||||
(ST f) <|> (ST g) = ST (\st => f st <|> g st)
|
||||
|
||||
public export
|
||||
implementation HasIO m => HasIO (StateT stateType m) where
|
||||
liftIO io = ST $ \s => liftIO $ io_bind io $ \a => pure (s, a)
|
||||
4
libs/base/Control/Monad/Writer.idr
Normal file
4
libs/base/Control/Monad/Writer.idr
Normal file
@ -0,0 +1,4 @@
|
||||
module Control.Monad.Writer
|
||||
|
||||
import public Control.Monad.Writer.Interface as Control.Monad.Writer
|
||||
import public Control.Monad.Writer.CPS as Control.Monad.Writer
|
||||
107
libs/base/Control/Monad/Writer/CPS.idr
Normal file
107
libs/base/Control/Monad/Writer/CPS.idr
Normal file
@ -0,0 +1,107 @@
|
||||
||| Note: The difference to a 'strict' Writer implementation is
|
||||
||| that accumulation of values does not happen in the
|
||||
||| Applicative and Monad instances but when invoking `Writer`-specific
|
||||
||| functions like `writer` or `listen`.
|
||||
module Control.Monad.Writer.CPS
|
||||
|
||||
import Control.Monad.Identity
|
||||
import Control.Monad.Trans
|
||||
|
||||
||| A writer monad parameterized by:
|
||||
|||
|
||||
||| @w the output to accumulate.
|
||||
|||
|
||||
||| @m The inner monad.
|
||||
|||
|
||||
||| The `pure` function produces the output `neutral`, while `>>=`
|
||||
||| combines the outputs of the subcomputations using `<+>`.
|
||||
public export
|
||||
record WriterT (w : Type) (m : Type -> Type) (a : Type) where
|
||||
constructor MkWriterT
|
||||
unWriterT : w -> m (a, w)
|
||||
|
||||
||| Construct an writer computation from a (result,output) computation.
|
||||
||| (The inverse of `runWriterT`.)
|
||||
public export %inline
|
||||
writerT : (Functor m, Semigroup w) => m (a, w) -> WriterT w m a
|
||||
writerT f = MkWriterT $ \w => (\(a,w') => (a,w <+> w')) <$> f
|
||||
|
||||
||| Unwrap a writer computation.
|
||||
||| (The inverse of 'writerT'.)
|
||||
public export %inline
|
||||
runWriterT : Monoid w => WriterT w m a -> m (a,w)
|
||||
runWriterT m = unWriterT m neutral
|
||||
|
||||
||| Extract the output from a writer computation.
|
||||
public export %inline
|
||||
execWriterT : (Functor m, Monoid w) => WriterT w m a -> m w
|
||||
execWriterT = map snd . runWriterT
|
||||
|
||||
||| Map both the return value and output of a computation using
|
||||
||| the given function.
|
||||
public export %inline
|
||||
mapWriterT : (Functor n, Monoid w, Semigroup w')
|
||||
=> (m (a, w) -> n (b, w')) -> WriterT w m a -> WriterT w' n b
|
||||
mapWriterT f m = MkWriterT \w =>
|
||||
(\(a,w') => (a,w <+> w')) <$> f (runWriterT m)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Writer Functions
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| The `return` function produces the output `neutral`, while `>>=`
|
||||
||| combines the outputs of the subcomputations using `<+>`.
|
||||
public export
|
||||
Writer : Type -> Type -> Type
|
||||
Writer w = WriterT w Identity
|
||||
|
||||
||| Unwrap a writer computation as a (result, output) pair.
|
||||
public export %inline
|
||||
runWriter : Monoid w => Writer w a -> (a, w)
|
||||
runWriter = runIdentity . runWriterT
|
||||
|
||||
||| Extract the output from a writer computation.
|
||||
public export %inline
|
||||
execWriter : Monoid w => Writer w a -> w
|
||||
execWriter = runIdentity . execWriterT
|
||||
|
||||
||| Map both the return value and output of a computation using
|
||||
||| the given function.
|
||||
public export %inline
|
||||
mapWriter : (Monoid w, Semigroup w')
|
||||
=> ((a, w) -> (b, w')) -> Writer w a -> Writer w' b
|
||||
mapWriter f = mapWriterT \(Id p) => Id (f p)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Implementations
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export %inline
|
||||
Functor m => Functor (WriterT w m) where
|
||||
map f m = MkWriterT \w => (\(a,w') => (f a,w')) <$> unWriterT m w
|
||||
|
||||
public export %inline
|
||||
Monad m => Applicative (WriterT w m) where
|
||||
pure a = MkWriterT \w => pure (a,w)
|
||||
MkWriterT mf <*> MkWriterT mx =
|
||||
MkWriterT \w => do (f,w1) <- mf w
|
||||
(a,w2) <- mx w1
|
||||
pure (f a,w2)
|
||||
|
||||
public export %inline
|
||||
(Monad m, Alternative m) => Alternative (WriterT w m) where
|
||||
empty = MkWriterT \_ => empty
|
||||
MkWriterT m <|> MkWriterT n = MkWriterT \w => m w <|> n w
|
||||
|
||||
public export %inline
|
||||
Monad m => Monad (WriterT w m) where
|
||||
m >>= k = MkWriterT \w => do (a,w1) <- unWriterT m w
|
||||
unWriterT (k a) w1
|
||||
|
||||
public export %inline
|
||||
MonadTrans (WriterT w) where
|
||||
lift m = MkWriterT \w => map (\a => (a,w)) m
|
||||
|
||||
public export %inline
|
||||
HasIO m => HasIO (WriterT w m) where
|
||||
liftIO = lift . liftIO
|
||||
117
libs/base/Control/Monad/Writer/Interface.idr
Normal file
117
libs/base/Control/Monad/Writer/Interface.idr
Normal file
@ -0,0 +1,117 @@
|
||||
module Control.Monad.Writer.Interface
|
||||
|
||||
import Control.Monad.Maybe
|
||||
import Control.Monad.Error.Either
|
||||
import Control.Monad.Reader.Reader
|
||||
import Control.Monad.State.State
|
||||
import Control.Monad.RWS.CPS
|
||||
import Control.Monad.Trans
|
||||
import Control.Monad.Writer.CPS
|
||||
|
||||
||| MonadWriter interface
|
||||
|||
|
||||
||| tell is like tell on the MUD's it shouts to monad
|
||||
||| what you want to be heard. The monad carries this 'packet'
|
||||
||| upwards, merging it if needed (hence the Monoid requirement).
|
||||
|||
|
||||
||| listen listens to a monad acting, and returns what the monad "said".
|
||||
|||
|
||||
||| pass lets you provide a writer transformer which changes internals of
|
||||
||| the written object.
|
||||
public export
|
||||
interface (Monoid w, Monad m) => MonadWriter w m | m where
|
||||
||| `writer (a,w)` embeds a simple writer action.
|
||||
writer : (a,w) -> m a
|
||||
writer (a, w) = tell w $> a
|
||||
|
||||
||| `tell w` is an action that produces the output `w`.
|
||||
tell : w -> m ()
|
||||
tell w = writer ((),w)
|
||||
|
||||
||| `listen m` is an action that executes the action `m` and adds
|
||||
||| its output to the value of the computation.
|
||||
listen : m a -> m (a, w)
|
||||
|
||||
||| `pass m` is an action that executes the action `m`, which
|
||||
||| returns a value and a function, and returns the value, applying
|
||||
||| the function to the output.
|
||||
pass : m (a, w -> w) -> m a
|
||||
|
||||
||| `listens f m` is an action that executes the action `m` and adds
|
||||
||| the result of applying @f@ to the output to the value of the computation.
|
||||
public export
|
||||
listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)
|
||||
listens f = map (\(a,w) => (a,f w)) . listen
|
||||
|
||||
||| `censor f m` is an action that executes the action `m` and
|
||||
||| applies the function `f` to its output, leaving the return value
|
||||
||| unchanged.
|
||||
public export
|
||||
censor : MonadWriter w m => (w -> w) -> m a -> m a
|
||||
censor f = pass . map (\a => (a,f))
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Implementations
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export %inline
|
||||
(Monoid w, Monad m) => MonadWriter w (WriterT w m) where
|
||||
writer = writerT . pure
|
||||
|
||||
listen m = MkWriterT \w =>
|
||||
(\(a,w') => ((a,w'),w <+> w')) <$> runWriterT m
|
||||
|
||||
tell w' = writer ((), w')
|
||||
|
||||
pass m = MkWriterT \w =>
|
||||
(\((a,f),w') => (a,w <+> f w')) <$> runWriterT m
|
||||
|
||||
public export %inline
|
||||
(Monoid w, Monad m) => MonadWriter w (RWST r w s m) where
|
||||
writer (a,w') = MkRWST \_,s,w => pure (a,s,w <+> w')
|
||||
|
||||
tell w' = writer ((), w')
|
||||
|
||||
listen m = MkRWST \r,s,w =>
|
||||
(\(a,s',w') => ((a,w'),s',w <+> w')) <$> runRWST m r s
|
||||
|
||||
pass m = MkRWST \r,s,w =>
|
||||
(\((a,f),s',w') => (a,s',w <+> f w')) <$> runRWST m r s
|
||||
|
||||
public export %inline
|
||||
MonadWriter w m => MonadWriter w (EitherT e m) where
|
||||
writer = lift . writer
|
||||
tell = lift . tell
|
||||
listen = mapEitherT \m => do (e,w) <- listen m
|
||||
pure $ map (\a => (a,w)) e
|
||||
|
||||
pass = mapEitherT \m => pass $ do Right (r,f) <- m
|
||||
| Left l => pure $ (Left l, id)
|
||||
pure (Right r, f)
|
||||
|
||||
public export %inline
|
||||
MonadWriter w m => MonadWriter w (MaybeT m) where
|
||||
writer = lift . writer
|
||||
tell = lift . tell
|
||||
listen = mapMaybeT \m => do (e,w) <- listen m
|
||||
pure $ map (\a => (a,w)) e
|
||||
|
||||
pass = mapMaybeT \m => pass $ do Just (r,f) <- m
|
||||
| Nothing => pure $ (Nothing, id)
|
||||
pure (Just r, f)
|
||||
public export %inline
|
||||
MonadWriter w m => MonadWriter w (ReaderT r m) where
|
||||
writer = lift . writer
|
||||
tell = lift . tell
|
||||
listen = mapReaderT listen
|
||||
pass = mapReaderT pass
|
||||
|
||||
public export %inline
|
||||
MonadWriter w m => MonadWriter w (StateT s m) where
|
||||
writer = lift . writer
|
||||
tell = lift . tell
|
||||
listen (ST m) = ST \s => do ((s',a),w) <- listen (m s)
|
||||
pure (s',(a,w))
|
||||
|
||||
pass (ST m) = ST \s => pass $ do (s',(a,f)) <- m s
|
||||
pure ((s',a),f)
|
||||
@ -5,12 +5,24 @@ modules = Control.App,
|
||||
Control.App.FileIO,
|
||||
|
||||
Control.Monad.Either,
|
||||
Control.Monad.Error.Either,
|
||||
Control.Monad.Error.Interface,
|
||||
Control.Monad.Identity,
|
||||
Control.Monad.Maybe,
|
||||
Control.Monad.RWS,
|
||||
Control.Monad.RWS.CPS,
|
||||
Control.Monad.RWS.Interface,
|
||||
Control.Monad.Reader,
|
||||
Control.Monad.Reader.Interface,
|
||||
Control.Monad.Reader.Reader,
|
||||
Control.Monad.ST,
|
||||
Control.Monad.State,
|
||||
Control.Monad.State.Interface,
|
||||
Control.Monad.State.State,
|
||||
Control.Monad.Trans,
|
||||
Control.Monad.Writer,
|
||||
Control.Monad.Writer.CPS,
|
||||
Control.Monad.Writer.Interface,
|
||||
Control.WellFounded,
|
||||
|
||||
Data.Bool,
|
||||
|
||||
Loading…
Reference in New Issue
Block a user