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

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

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

module Effect.Monad where

open import Data.Bool.Base using (Bool; true; false; not)
open import Data.Unit.Polymorphic.Base using (⊤)
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Applicative as App
  using (RawApplicative; RawApplicativeZero; mkRawApplicative; RawAlternative)
open import Function.Base using (id; flip; _$′_; _∘′_)
open import Level using (Level; suc; _⊔_)

private
  variable
    f g g₁ g₂ : Level
    A B C : Set f

------------------------------------------------------------------------
-- The type of raw monads

record RawMonad (F : Set f → Set g) : Set (suc f ⊔ g) where
  infixl  _>>=_ _>>_ _>=>_
  infixr  _=<<_ _<=<_
  field
    rawApplicative : RawApplicative F
    _>>=_ : F A → (A → F B) → F B

  open RawApplicative rawApplicative public

  _>>_ : F A → F B → F B
  _>>_ = _*>_

  _=<<_ : (A → F B) → F A → F B
  _=<<_ = flip _>>=_

  Kleisli : Set f → Set f → Set (f ⊔ g)
  Kleisli A B = A → F B

  _>=>_ : Kleisli A B → Kleisli B C → Kleisli A C
  (f >=> g) a = f a >>= g

  _<=<_ : Kleisli B C → Kleisli A B → Kleisli A C
  _<=<_ = flip _>=>_

  when : Bool → F ⊤ → F ⊤
  when true m = m
  when false m = pure _

  unless : Bool → F ⊤ → F ⊤
  unless = when ∘′ not

-- When level g=f, a join/μ operator is definable

module Join {F : Set f → Set f} (M : RawMonad F) where
  open RawMonad M

  join : F (F A) → F A
  join = _>>= id

-- Smart constructor

module _ where

  open RawMonad
  open RawApplicative

  mkRawMonad :
    (F : Set f → Set g) →
    (pure : ∀ {A} → A → F A) →
    (bind : ∀ {A B} → F A → (A → F B) → F B) →
    RawMonad F
  mkRawMonad F pure _>>=_ .rawApplicative =
    mkRawApplicative _ pure $′ λ mf mx → do
      f ← mf
      x ← mx
      pure (f x)
  mkRawMonad F pure _>>=_ ._>>=_ = _>>=_

------------------------------------------------------------------------
-- The type of raw monads with a zero

record RawMonadZero (F : Set f → Set g) : Set (suc f ⊔ g) where
  field
    rawMonad : RawMonad F
    rawEmpty : RawEmpty F

  open RawMonad rawMonad public
  open RawEmpty rawEmpty public

  rawApplicativeZero : RawApplicativeZero F
  rawApplicativeZero = record
    { rawApplicative = rawApplicative
    ; rawEmpty = rawEmpty
    }

------------------------------------------------------------------------
-- The type of raw monadplus

record RawMonadPlus (F : Set f → Set g) : Set (suc f ⊔ g) where
  field
    rawMonadZero : RawMonadZero F
    rawChoice    : RawChoice F

  open RawMonadZero rawMonadZero public
  open RawChoice rawChoice public

  rawAlternative : RawAlternative F
  rawAlternative = record
    { rawApplicativeZero = rawApplicativeZero
    ; rawChoice = rawChoice
    }

------------------------------------------------------------------------
-- The type of raw monad transformer

-- F has been RawMonadT'd as TF
record RawMonadTd (F : Set f → Set g₁) (TF : Set f → Set g₂) : Set (suc f ⊔ g₁ ⊔ g₂) where
  field
    lift : F A → TF A
    rawMonad : RawMonad TF

  open RawMonad rawMonad public

RawMonadT : (T : (Set f → Set g₁) → (Set f → Set g₂)) → Set (suc f ⊔ suc g₁ ⊔ g₂)
RawMonadT T = ∀ {M} → RawMonad M → RawMonadTd M (T M)