------------------------------------------------------------------------
-- 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 {a} (A : Set a) (b : Level) where
 
open import Data.Sum.Base using (map₂ ; inj₁ ; inj₂; _⊎_; [_,_]′)
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative
  using (RawApplicative; RawApplicativeZero; RawAlternative)
open import Effect.Monad using (RawMonad; module Join)
open import Function.Base using (const; flip; _∘_; _∘′_; _$_; _|>′_)
 
-- 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.
 
------------------------------------------------------------------------
-- Left-biased monad instance for _⊎_
 
Sumₗ : Set (a ⊔ b) → Set (a ⊔ b)
Sumₗ B = A ⊎ B
 
functor : RawFunctor Sumₗ
functor = record { _<$>_ = map₂ }
 
applicative : RawApplicative Sumₗ
applicative = record
  { rawFunctor = functor
  ; pure = inj₂
  ; _<*>_ = [ const ∘ inj₁ , map₂ ]′
  }
 
empty : A → RawEmpty Sumₗ
empty a = record { empty = inj₁ a }
 
choice : RawChoice Sumₗ
choice = record { _<|>_ = [ flip const , const ∘ inj₂ ]′ }
 
applicativeZero : A → RawApplicativeZero Sumₗ
applicativeZero a = record
  { rawApplicative = applicative
  ; rawEmpty = empty a
  }
 
alternative : A → RawAlternative Sumₗ
alternative a = record
  { rawApplicativeZero = applicativeZero a
  ; rawChoice = choice
  }
 
monad : RawMonad Sumₗ
monad = record
  { rawApplicative = applicative
  ; _>>=_ = [ const ∘′ inj₁ , _|>′_ ]′
  }
 
join : {B : Set (a ⊔ b)} → Sumₗ (Sumₗ B) → Sumₗ B
join = Join.join monad
 
------------------------------------------------------------------------
-- Get access to other monadic functions
 
module TraversableA {F} (App : RawApplicative {a ⊔ b} {a ⊔ b} F) where
 
  open RawApplicative App
 
  sequenceA : ∀ {A} → Sumₗ (F A) → F (Sumₗ A)
  sequenceA (inj₁ a) = pure (inj₁ a)
  sequenceA (inj₂ x) = inj₂ <$> x
 
  mapA : ∀ {A B} → (A → F B) → Sumₗ A → F (Sumₗ B)
  mapA f = sequenceA ∘ map₂ f
 
  forA : ∀ {A B} → Sumₗ A → (A → F B) → F (Sumₗ B)
  forA = flip mapA
 
module TraversableM {M} (Mon : RawMonad {a ⊔ b} {a ⊔ b} M) where
 
  open RawMonad Mon
 
  open TraversableA rawApplicative public
    renaming
    ( sequenceA to sequenceM
    ; mapA      to mapM
    ; forA      to forM
    )