------------------------------------------------------------------------
-- The Agda standard library
--
-- Universe-sensitive functor and monad instances for the Product type.
------------------------------------------------------------------------

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

open import Algebra

module Data.Product.Effectful.Examples
  {a e b} {A : Monoid a e} {B : Set b} where

open import Level using (Lift; lift; _⊔_)
open import Effect.Functor using (RawFunctor)
open import Effect.Monad using (RawMonad)
open import Data.Product.Base using (_×_; _,_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Function.Base using (id)
import Function.Identity.Effectful as Id
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

------------------------------------------------------------------------
-- Examples

-- Note that these examples are simple unit tests, because the type
-- checker verifies them.

private

  module A = Monoid A

  open import Data.Product.Effectful.Left A.rawMonoid b

  _≈_ : Rel (A.Carrier × Lift a B) (e ⊔ a ⊔ b)
  _≈_ = Pointwise A._≈_ _≡_

  open RawFunctor functor

  -- This type to the right of × needs to be a "lifted" version of
  -- (B : Set b) that lives in the universe (Set (a ⊔ b)).
  fmapIdₗ : (x : A.Carrier × Lift a B) → (id <$> x) ≈ x
  fmapIdₗ x = A.refl , refl

  open RawMonad monad

  -- Now, let's show that "pure" is a unit for >>=. We use Lift in
  -- exactly the same way as above. The data (x : B) then needs to be
  -- "lifted" to this new type (Lift B).
  pureUnitL : ∀ {x : B} {f : Lift a B → A.Carrier × Lift a B} →
                (pure (lift x) >>= f) ≈ f (lift x)
  pureUnitL = A.identityˡ _ , refl

  pureUnitR : {x : A.Carrier × Lift a B} → (x >>= pure) ≈ x
  pureUnitR = A.identityʳ _ , refl

  -- And another (limited version of a) monad law...
  bindCompose : ∀ {f g : Lift a B → A.Carrier × Lift a B} →
                {x : A.Carrier × Lift a B} →
                ((x >>= f) >>= g) ≈ (x >>= (λ y → (f y >>= g)))
  bindCompose = A.assoc _ _ _ , refl