Source code on Github
{-# OPTIONS --cubical-compatible #-}
module Class.Monad.Core where

open import Class.Prelude
open import Class.Core
open import Class.Functor
open import Class.Applicative

record Monad (M : Type↑) : Typeω where
  infixl 1 _>>=_ _>>_ _>=>_
  infixr 1 _=<<_ _<=<_

  field
    overlap  super  : Applicative M
    return : A  M A
    _>>=_  : M A  (A  M B)  M B

  _>>_ : M A  M B  M B
  m₁ >> m₂ = m₁ >>= λ _  m₂

  _=<<_ : (A  M B)  M A  M B
  f =<< c = c >>= f

  _≫=_ = _>>=_; _≫_ = _>>_; _=≪_ = _=<<_

  _>=>_ : (A  M B)  (B  M C)  (A  M C)
  f >=> g = _=<<_ g  f

  _<=<_ : (B  M C)  (A  M B)  (A  M C)
  g <=< f = f >=> g

  join : M (M A)  M A
  join m = m >>= id

  Functor-M : Functor M
  Functor-M = λ where ._<$>_ f x  return  f =<< x

open Monad ⦃...⦄ public

module _  _ : Monad M  where
  mapM : (A  M B)  List A  M (List B)
  mapM f []       = return []
  mapM f (x  xs) =  f x  mapM f xs 

  concatMapM : (A  M (List B))  List A  M (List B)
  concatMapM f xs = concat <$> mapM f xs

  forM : List A  (A  M B)  M (List B)
  forM []       _ = return []
  forM (x  xs) f =  f x  forM xs f 

  concatForM : List A  (A  M (List B))  M (List B)
  concatForM xs f = concat <$> forM xs f

  return⊤ void : M A  M 
  return⊤ k = k  return tt
  void = return⊤

  filterM : (A  M Bool)  List A  M (List A)
  filterM _ [] = return []
  filterM p (x  xs) = do
    b  p x
    ((if b then [ x ] else []) ++_) <$> filterM p xs

  traverseM : (A  M B)  List A  M (List B)
  traverseM f = λ where
    []  return []
    (x  xs)   f x  traverseM f xs 

record MonadLaws (M : Type↑)  _ : Monad M  : Typeω where
  field
    >>=-identityˡ :  {A : Type } {B : Type ℓ′} 
       {a : A} {h : A  M B} 
        (return a >>= h)  h a
    >>=-identityʳ :  {A : Type } 
       (m : M A) 
        (m >>= return)  m
    >>=-assoc :  {A : Type } {B : Type ℓ′} {C : Type ℓ″} 
       (m : M A) {g : A  M B} {h : B  M C} 
        ((m >>= g) >>= h)  (m >>=  x  g x >>= h))
open MonadLaws ⦃...⦄ public

record Monad₀ (M : Type↑) : Typeω where
  field  isMonad  : Monad M
         isApplicative₀  : Applicative₀ M
open Monad₀ ⦃...⦄ using () public
instance
  mkMonad₀ :  Monad M    Applicative₀ M   Monad₀ M
  mkMonad₀ = record {}

record Monad⁺ (M : Type↑) : Typeω where
  field  isMonad  : Monad M
         isAlternative  : Alternative M
open Monad⁺ ⦃...⦄ using () public
instance
  mkMonad⁺ :  Monad M    Alternative M   Monad⁺ M
  mkMonad⁺ = record {}