------------------------------------------------------------------------ -- 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 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 -- 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)