------------------------------------------------------------------------
-- The Agda standard library
--
-- Left-biased universe-sensitive functor and monad instances for the
-- Product type.
--
-- 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 Data.Product.Effectful.Examples for how this is
-- done.
------------------------------------------------------------------------

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

open import Algebra
open import Level

module Data.Product.Effectful.Left
  {a e} (A : RawMonoid a e) (b : Level) where

open import Data.Product.Base
import Data.Product.Effectful.Left.Base as Base
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad; RawMonadT; mkRawMonad)
open import Function.Base using (id; flip; _∘_; _∘′_)
import Function.Identity.Effectful as Id

open RawMonoid A

------------------------------------------------------------------------
-- Re-export the base contents publically

open Base Carrier b public

------------------------------------------------------------------------
-- Basic records

applicative : RawApplicative Productₗ
applicative = record
  { rawFunctor = functor
  ; pure = ε ,_
  ; _<*>_  = zip _∙_ id
  }

monad : RawMonad Productₗ
monad = record
  { rawApplicative = applicative
  ; _>>=_ = uncurry λ w₁ a f → map₁ (w₁ ∙_) (f a)
  }

-- The monad instance also requires some mucking about with universe levels.
monadT : ∀ {ℓ} → RawMonadT {g₁ = ℓ} (_∘′ Productₗ)
monadT M = record
  { lift = (ε ,_) <$>_
  ; rawMonad = mkRawMonad _
                 (pure ∘′ (ε ,_))
                 (λ ma f → ma >>= uncurry λ a x → map₁ (a ∙_) <$> f x)
  } where open RawMonad M

------------------------------------------------------------------------
-- Get access to other monadic functions

module TraversableA {F} (App : RawApplicative {a ⊔ b} {a ⊔ b} F) where

  open RawApplicative App

  sequenceA : ∀ {A} → Productₗ (F A) → F (Productₗ A)
  sequenceA (x , fa) = (x ,_) <$> fa

  mapA : ∀ {A B} → (A → F B) → Productₗ A → F (Productₗ B)
  mapA f = sequenceA ∘ map₂ f

  forA : ∀ {A B} → Productₗ A → (A → F B) → F (Productₗ 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
    )