------------------------------------------------------------------------
-- The Agda standard library
--
-- The writer monad transformer
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Effect.Monad.Writer.Transformer where
open import Algebra using (RawMonoid)
open import Data.Product.Base using (_×_; _,_; proj₂; map₂)
open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Functor using (RawFunctor)
open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus; RawMonadT)
open import Function.Base using (_∘′_; const; _$_)
open import Level using (Level)
private
variable
w g g₁ g₂ : Level
A B : Set w
M : Set w → Set g
𝕎 : RawMonoid w g
------------------------------------------------------------------------
-- Re-export the basic type definitions
open import Effect.Monad.Writer.Transformer.Base public
using ( RawMonadWriter
; WriterT
; mkWriterT
; runWriterT
)
------------------------------------------------------------------------
-- Structure
functor : RawFunctor M → RawFunctor (WriterT 𝕎 M)
functor M = record
{ _<$>_ = λ f ma → mkWriterT λ w → map₂ f <$> runWriterT ma w
} where open RawFunctor M
empty : RawEmpty M → RawEmpty (WriterT 𝕎 M)
empty M = record
{ empty = mkWriterT (const (RawEmpty.empty M))
}
choice : RawChoice M → RawChoice (WriterT 𝕎 M)
choice M = record
{ _<|>_ = λ ma₁ ma₂ → mkWriterT λ w →
WriterT.runWriterT ma₁ w
<|> WriterT.runWriterT ma₂ w
} where open RawChoice M
module _ {𝕎 : RawMonoid w g} where
open RawMonoid 𝕎 renaming (Carrier to W)
applicative : RawApplicative M → RawApplicative (WriterT 𝕎 M)
applicative M = record
{ rawFunctor = functor rawFunctor
; pure = λ a → mkWriterT (pure ∘′ (_, a))
; _<*>_ = λ mf mx → mkWriterT $ λ w →
(go <$> runWriterT mf w) <*> runWriterT mx ε
} where
open RawApplicative M
go : W × (A → B) → W × A → W × B
go (w₁ , f) (w₂ , x) = w₁ ∙ w₂ , f x
applicativeZero : RawApplicativeZero M → RawApplicativeZero (WriterT 𝕎 M)
applicativeZero M = record
{ rawApplicative = applicative rawApplicative
; rawEmpty = empty rawEmpty
} where open RawApplicativeZero M using (rawApplicative; rawEmpty)
alternative : RawAlternative M → RawAlternative (WriterT 𝕎 M)
alternative M = record
{ rawApplicativeZero = applicativeZero rawApplicativeZero
; rawChoice = choice rawChoice
} where open RawAlternative M
monad : RawMonad M → RawMonad (WriterT 𝕎 M)
monad M = record
{ rawApplicative = applicative rawApplicative
; _>>=_ = λ ma f → mkWriterT λ w → do
w₁ , a ← runWriterT ma w
runWriterT (f a) w₁
} where open RawMonad M
monadZero : RawMonadZero M → RawMonadZero (WriterT 𝕎 M)
monadZero M = record
{ rawMonad = monad (RawMonadZero.rawMonad M)
; rawEmpty = empty (RawMonadZero.rawEmpty M)
}
monadPlus : RawMonadPlus M → RawMonadPlus (WriterT 𝕎 M)
monadPlus M = record
{ rawMonadZero = monadZero rawMonadZero
; rawChoice = choice rawChoice
} where open RawMonadPlus M
----------------------------------------------------------------------
-- Monad writer transformer specifics
monadT : RawMonadT {g₁ = g₁} {g₂ = _} (WriterT 𝕎)
monadT M = record
{ lift = mkWriterT ∘′ λ ma w → (w ,_) <$> ma
; rawMonad = monad M
} where open RawMonad M
monadWriter : RawMonad M → RawMonadWriter 𝕎 (WriterT 𝕎 M)
monadWriter M = record
{ writer = mkWriterT ∘′ λ (w' , a) w → pure (w ∙ w' , a)
; listen = λ ma → mkWriterT λ w → do
w , a ← runWriterT ma w
pure (w , w , a)
; pass = λ mx → mkWriterT λ w → do
w , f , a ← runWriterT mx w
pure (f w , a)
} where open RawMonad M
module _ {𝕎₁ : RawMonoid w g₁} where
open RawMonoid 𝕎₁ renaming (Carrier to W₁)
liftWriterT : (𝕎₂ : RawMonoid w g₂) →
RawFunctor M →
RawMonadWriter 𝕎₁ M →
RawMonadWriter 𝕎₁ (WriterT 𝕎₂ M)
liftWriterT 𝕎₂ M MWrite = record
{ writer = λ (w , a) → mkWriterT λ w' → (writer (w , w' , a ))
; listen = λ mx → mkWriterT λ w' → ((λ (w₁ , w₂ , a) → w₂ , w₁ , a) <$> listen (runWriterT mx w'))
; pass = λ mx → mkWriterT λ w' → (pass ((λ (w , f , a) → f , w , a) <$> runWriterT mx w'))
} where open RawMonadWriter MWrite
open RawFunctor M
private
variable
W₂ : Set g₂
open import Effect.Monad.Reader.Transformer.Base
liftReaderT : RawFunctor M →
RawMonadWriter 𝕎₁ M →
RawMonadWriter 𝕎₁ (ReaderT W₂ M)
liftReaderT M MWrite = record
{ writer = mkReaderT ∘′ const ∘′ writer
; listen = λ ma → mkReaderT (listen ∘′ runReaderT ma)
; pass = λ ma → mkReaderT (pass ∘′ runReaderT ma)
} where open RawMonadWriter MWrite
open import Effect.Monad.State.Transformer.Base
liftStateT : RawFunctor M →
RawMonadWriter 𝕎₁ M →
RawMonadWriter 𝕎₁ (StateT W₂ M)
liftStateT M MWrite = record
{ writer = λ x → mkStateT λ w₂ → (w₂ ,_) <$>
writer x
; listen = λ mx → mkStateT λ w₂ → (w₂ ,_) <$>
listen (proj₂ <$> runStateT mx w₂)
; pass = λ mx → mkStateT λ w₂ → (w₂ ,_) <$>
pass ((λ (_ , f , a) → f , a) <$> runStateT mx w₂)
} where open RawMonadWriter MWrite
open RawFunctor M
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4