Skip to content

Effect.Monad.Writer.Transformer

------------------------------------------------------------------------
-- 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