------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed monads
------------------------------------------------------------------------

-- Note that currently the monad laws are not included here.

{-# OPTIONS --without-K --safe #-}

module Category.Monad.Indexed where

open import Category.Applicative.Indexed
open import Function
open import Level

record RawIMonad {i f} {I : Set i} (M : IFun I f) :
                 Set (i ⊔ suc f) where
  infixl  _>>=_ _>>_ _>=>_
  infixr  _=<<_ _<=<_

  field
    return : ∀ {i A} → A → M i i A
    _>>=_  : ∀ {i j k A B} → M i j A → (A → M j k B) → M i k B

  _>>_ : ∀ {i j k A B} → M i j A → M j k B → M i k B
  m₁ >> m₂ = m₁ >>= λ _ → m₂

  _=<<_ : ∀ {i j k A B} → (A → M j k B) → M i j A → M i k B
  f =<< c = c >>= f

  _>=>_ : ∀ {i j k a} {A : Set a} {B C} →
          (A → M i j B) → (B → M j k C) → (A → M i k C)
  f >=> g = _=<<_ g ∘ f

  _<=<_ : ∀ {i j k B C a} {A : Set a} →
          (B → M j k C) → (A → M i j B) → (A → M i k C)
  g <=< f = f >=> g

  join : ∀ {i j k A} → M i j (M j k A) → M i k A
  join m = m >>= id

  rawIApplicative : RawIApplicative M
  rawIApplicative = record
    { pure = return
    ; _⊛_  = λ f x → f >>= λ f' → x >>= λ x' → return (f' x')
    }

  open RawIApplicative rawIApplicative public

RawIMonadT : ∀ {i f} {I : Set i} (T : IFun I f → IFun I f) → Set (i ⊔ suc f)
RawIMonadT T = ∀ {M} → RawIMonad M → RawIMonad (T M)

record RawIMonadZero {i f} {I : Set i} (M : IFun I f) :
                     Set (i ⊔ suc f) where
  field
    monad : RawIMonad M
    ∅     : ∀ {i j A} → M i j A

  open RawIMonad monad public

record RawIMonadPlus {i f} {I : Set i} (M : IFun I f) :
                     Set (i ⊔ suc f) where
  infixr  _∣_
  field
    monadZero : RawIMonadZero M
    _∣_       : ∀ {i j A} → M i j A → M i j A → M i j A

  open RawIMonadZero monadZero public