module Library.Monad where
open import Agda.Primitive
open import Agda.Builtin.Unit
record Functor {a b} (F : Set a → Set b) : Set (lsuc a ⊔ b) where
infixl 4 _<$>_
field
fmap : ∀ {A B} → (A → B) → F A → F B
_<$>_ = fmap
open Functor {{...}} public
record IApplicative {i a b} {I : Set i} (F : I → I → Set a → Set b) : Set (i ⊔ lsuc a ⊔ b) where
infixl 4 _<*>_
field
pure : ∀ {i A} → A → F i i A
_<*>_ : ∀ {i j k A B} → F i j (A → B) → F j k A → F i k B
overlap {{super}} : ∀ {i j} → Functor (F i j)
open IApplicative {{...}} public
Applicative : ∀ {a b} (M : Set a → Set b) → Set (lsuc a ⊔ b)
Applicative F = IApplicative {I = ⊤} (λ _ _ → F)
record IMonad {i a b} {I : Set i} (M : I → I → Set a → Set b) : Set (i ⊔ lsuc a ⊔ b) where
infixl 1 _>>=_ _>>_
infixr 1 _=<<_
field
_>>=_ : ∀ {i j k A B} → M i j A → (A → M j k B) → M i k B
overlap {{super}} : IApplicative {I = I} M
return : ∀ {i A} → A → M i i A
return = pure
_>>_ : ∀ {i j k A B} → M i j A → M j k B → M i k B
m₁ >> m₂ = m₁ >>= λ _ → m₂
_=<<_ : ∀ {i j k A B} → (A → M j k B) → M i j A → M i k B
f =<< m = m >>= f
open IMonad {{...}} public
Monad : ∀ {a b} (M : Set a → Set b) → Set (lsuc a ⊔ b)
Monad M = IMonad {I = ⊤} (λ _ _ → M)
open import Data.Maybe using (Maybe; nothing; just)
instance
functorMaybe : ∀ {a} → Functor (Maybe {a})
functorMaybe .fmap f = λ where
(just x) → just (f x)
nothing → nothing
applicativeMaybe : ∀ {a} → Applicative (Maybe {a})
applicativeMaybe .pure = just
applicativeMaybe ._<*>_ = λ where
(just f) x → fmap f x
nothing x → nothing
monadMaybe : ∀ {a} → Monad (Maybe {a})
monadMaybe ._>>=_ = λ where
(just x) f → f x
nothing f → nothing