------------------------------------------------------------------------
-- Raw monads
------------------------------------------------------------------------

-- Note that this module is not parametrised by an axiomatisation of
-- equality. This module is reexported from Monad.

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

module Monad.Raw where

open import Prelude

-- Raw monads.

record Raw-monad {d c} (M : Type d → Type c) : Type (lsuc d ⊔ c) where
  constructor mk
  infixl  _⟨$⟩_ _⊛_
  infixl  _>>=_ _>>_
  infixr  _=<<_
  field
    return : ∀ {A} → A → M A
    _>>=_  : ∀ {A B} → M A → (A → M B) → M B

  -- Variants of _>>=_.

  _>>_ : ∀ {A B} → M A → M B → M B
  x >> y = x >>= const y

  _=<<_ : ∀ {A B} → (A → M B) → M A → M B
  _=<<_ = flip _>>=_

  -- A map function.

  map : ∀ {A B} → (A → B) → M A → M B
  map f x = x >>= return ∘ f

  -- A synonym.

  _⟨$⟩_ : ∀ {A B} → (A → B) → M A → M B
  _⟨$⟩_ = map

  -- Applicative functor application.

  _⊛_ : ∀ {A B} → M (A → B) → M A → M B
  f ⊛ x = f >>= λ f → x >>= λ x → return (f x)

  -- The sequence function (for lists).

  sequence : ∀ {A} → List (M A) → M (List A)
  sequence []       = return []
  sequence (x ∷ xs) = _∷_ ⟨$⟩ x ⊛ sequence xs

open Raw-monad ⦃ … ⦄ public

-- Raw monad transformers.

record Raw-monad-transformer
         {d c₁ c₂} (F : (Type d → Type c₁) → (Type d → Type c₂)) :
         Type (lsuc (c₁ ⊔ d) ⊔ c₂) where
  constructor mk
  field
    transform : ∀ {M}   ⦃ is-raw-monad : Raw-monad M ⦄ → Raw-monad (F M)
    liftʳ     : ∀ {M A} ⦃ is-raw-monad : Raw-monad M ⦄ → M A → F M A

open Raw-monad-transformer ⦃ … ⦄ public using (liftʳ)