------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of the Sum type (Right-biased)
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Level

module Data.Sum.Effectful.Right.Transformer (a : Level) {b} (B : Set b) where

open import Data.Sum.Base
open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Function.Base

private
  variable
    M : Set (a ⊔ b) → Set (a ⊔ b)

-- To minimize the universe level of the RawFunctor, we require that
-- elements of B are "lifted" to a copy of B at a higher universe level
-- (a ⊔ b). See the examples for how this is done.

open import Data.Sum.Effectful.Right a B using (Sumᵣ)

------------------------------------------------------------------------
-- Right-biased monad transformer instance for _⊎_

record SumᵣT
         (M : Set (a ⊔ b) → Set (a ⊔ b))
         (B : Set (a ⊔ b)) : Set (a ⊔ b) where
  constructor mkSumᵣT
  field runSumᵣT : M (Sumᵣ B)
open SumᵣT public

------------------------------------------------------------------------
-- Structure

functor : RawFunctor M → RawFunctor (SumᵣT M)
functor M = record
  { _<$>_ = λ f → mkSumᵣT ∘′ (map₁ f <$>_) ∘′ runSumᵣT
  } where open RawFunctor M

applicative : RawApplicative M → RawApplicative (SumᵣT M)
applicative M = record
  { rawFunctor = functor rawFunctor
  ; pure = mkSumᵣT ∘′ pure ∘′ inj₁
  ; _<*>_ = λ mf mx → mkSumᵣT ([ map₁ , const ∘′ inj₂ ]′ <$> runSumᵣT mf <*> runSumᵣT mx)
  } where open RawApplicative M

empty : RawApplicative M → B → RawEmpty (SumᵣT M)
empty M a = record
  { empty = mkSumᵣT (pure (inj₂ a))
  } where open RawApplicative M

choice : RawApplicative M → RawChoice (SumᵣT M)
choice M = record
  { _<|>_ = λ ma₁ ma₁ → mkSumᵣT ([ const ∘ inj₁ , flip const ]′ <$> runSumᵣT ma₁ <*> runSumᵣT ma₁)
  } where open RawApplicative M

applicativeZero : RawApplicative M → B → RawApplicativeZero (SumᵣT M)
applicativeZero M a = record
  { rawApplicative = applicative M
  ; rawEmpty = empty M a
  }

alternative : RawApplicative M → B → RawAlternative (SumᵣT M)
alternative M a = record
  { rawApplicativeZero = applicativeZero M a
  ; rawChoice = choice M
  }

monad : RawMonad M → RawMonad (SumᵣT M)
monad M = record
  { rawApplicative = applicative rawApplicative
  ; _>>=_ = λ ma f → mkSumᵣT $ do
                       a ← runSumᵣT ma
                       [ runSumᵣT ∘′ f , pure ∘′ inj₂ ]′ a
  } where open RawMonad M

monadT : RawMonadT SumᵣT
monadT M = record
  { lift = mkSumᵣT ∘′ (inj₁ <$>_)
  ; rawMonad = monad M
  } where open RawMonad M