------------------------------------------------------------------------
-- The Agda standard library
--
-- The writer monad
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Effect.Monad.Writer where
open import Algebra using (RawMonoid)
open import Data.Product.Base using (_×_)
open import Effect.Applicative using (RawApplicative)
open import Effect.Functor using (RawFunctor)
open import Effect.Monad using (RawMonad; module Join)
open import Effect.Monad.Identity as Id using (Identity; runIdentity)
open import Level using (Level)
import Effect.Monad.Writer.Transformer as Trans
private
variable
w ℓ : Level
A : Set w
𝕎 : RawMonoid w ℓ
------------------------------------------------------------------------
-- Re-export the monad writer operations
open Trans public
using (RawMonadWriter)
------------------------------------------------------------------------
-- Writer monad
Writer : (𝕎 : RawMonoid w ℓ) (A : Set w) → Set w
Writer 𝕎 = Trans.WriterT 𝕎 Identity
functor : RawFunctor (Writer 𝕎)
functor = Trans.functor Id.functor
module _ {𝕎 : RawMonoid w ℓ} where
open RawMonoid 𝕎 renaming (Carrier to W)
runWriter : Writer 𝕎 A → W × A
runWriter ma = runIdentity (Trans.runWriterT ma ε)
applicative : RawApplicative (Writer 𝕎)
applicative = Trans.applicative Id.applicative
monad : RawMonad (Writer 𝕎)
monad = Trans.monad Id.monad
join : Writer 𝕎 (Writer 𝕎 A) → Writer 𝕎 A
join = Join.join monad
----------------------------------------------------------------------
-- Writer monad specifics
monadWriter : RawMonadWriter 𝕎 (Writer 𝕎)
monadWriter = Trans.monadWriter Id.monad
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