------------------------------------------------------------------------
-- The Agda standard library
--
------------------------------------------------------------------------

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

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

open import Effect.Applicative.Indexed
open import Function.Base
open import Level

private
variable
a b c i f : Level
A : Set a
B : Set b
C : Set c
I : Set i

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

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

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

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

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

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

join :  {i j k}  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 : Set i} (T : IFun I f  IFun I f)  Set (i  suc f)

record RawIMonadZero {I : Set i} (M : IFun I f) : Set (i  suc f) where
field
applicativeZero : RawIApplicativeZero M

open RawIApplicativeZero applicativeZero using () public

record RawIMonadPlus {I : Set i} (M : IFun I f) : Set (i  suc f) where
field
alternative : RawIAlternative M

open RawIAlternative alternative using (; _∣_) public