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

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

open import Level

module Data.Sum.Effectful.Left.Transformer {a} (A : Set a) (b : Level) 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.Left A b using (Sumₗ)

------------------------------------------------------------------------
-- Left-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 ([ const ∘′ inj₁ , map₂ ]′ <$> runSumₗT mf <*> runSumₗT mx)
  } where open RawApplicative M

empty : RawApplicative M → A → 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 ([ flip const , const ∘ inj₂ ]′ <$> runSumₗT ma₁ <*> runSumₗT ma₂)
  } where open RawApplicative M

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

alternative : RawApplicative M → A → 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
                       [ pure ∘′ inj₁ , runSumₗT ∘′ f ]′ a
  } where open RawMonad M

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