{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude
open import Bool
open import List

module MonadPlus (M : Set → Set)

       (_>>=_  : {A B : Set} → M A → (A → M B) → M B)
       (return : {A : Set} → A → M A)
       (plus   : {A : Set} → M A → M A → M A)
       (zero   : {A : Set} → M A)

-- monad laws

       (1stLaw : {A B : Set} → {a : A} → {f : A → M B} → return a >>= f ≡ f a)
       (2ndLaw : {A : Set} → {ma : M A} → Extensionality → ma >>= return ≡ ma)
       (3rdLaw : {A B C : Set} → {f : A → M B} → {g : B → M C} → Extensionality → (ma : M A) → (ma >>= f) >>= g ≡ ma >>= (λ b → f b >>= g))

       (4thLaw : {A B : Set} → {f : A → M B} → zero >>= f ≡ zero)
       (5thLaw : {A B : Set} → (ma : M A) → ma >>= (λ a → zero {B}) ≡ zero {B})

       (6thLaw : {A : Set} → {ma : M A} → plus zero ma ≡ ma)
       (7thLaw : {A : Set} → {ma : M A} → plus ma zero ≡ ma)

where

import Monad
open Monad M _>>=_ return 1stLaw 2ndLaw 3rdLaw public

mplus : {A : Set} → M A → M A → M A
mplus = plus

mzero : {A : Set} → M A
mzero = zero

msum : {A : Set} → List (M A) → M A
msum = foldl plus zero

guard : Bool → M Unit
guard false = zero
guard true  = return unit