{-# 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
open import Effect.Empty
open import Effect.Applicative
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
record RawMonad (F : Set f → Set g) : Set (suc f ⊔ g) where
infixl 1 _>>=_ _>>_ _>=>_
infixr 1 _=<<_ _<=<_
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
module Join {F : Set f → Set f} (M : RawMonad F) where
open RawMonad M
join : F (F A) → F A
join = _>>= id
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 _>>=_ ._>>=_ = _>>=_
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
}
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
}
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)