mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 08:42:11 +03:00
108 lines
3.6 KiB
Idris
108 lines
3.6 KiB
Idris
||| Note: The difference to a 'stricht' 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
|