Source code on Github{-# OPTIONS --safe --without-K #-}
open import Meta.Prelude
open import Class.Functor
open import Class.Applicative
open import Class.Monad
open import Reflection using (TC; ErrorPart; typeError; catchTC; strErr)
module Class.MonadError where
private variable e f : Level
record MonadError (E : Set e) (M : ∀ {f} → Set f → Set f) : Setω where
field
error : E → M A
catch : M A → (E → M A) → M A
open MonadError
MonadError-TC : MonadError (List ErrorPart) TC
MonadError-TC .error = typeError
MonadError-TC .catch x h = catchTC x (h [ strErr "TC doesn't provide which error to catch" ])
ErrorT : (E : Set) → (M : ∀ {f} → Set f → Set f) → ∀ {f} → Set f → Set f
ErrorT E M A = M (E ⊎ A)
import Data.Sum as Sum
module _ {E : Set} {M : ∀ {a} → Set a → Set a} where
Functor-ErrorT : ⦃ _ : Functor M ⦄ → Functor (ErrorT E M)
Functor-ErrorT ._<$>_ f = fmap (Sum.map₂ f)
instance _ = Functor-ErrorT
Applicative-ErrorT : ⦃ _ : Applicative M ⦄ → Applicative (ErrorT E M)
Applicative-ErrorT .pure a = pure (inj₂ a)
Applicative-ErrorT ._<*>_ f x = _<*>_ {F = M} (fmap go f) x
where
go : (E ⊎ (A → B)) → (E ⊎ A) → (E ⊎ B)
go = λ where
(inj₁ e) _ → inj₁ e
_ (inj₁ e) → inj₁ e
(inj₂ f) (inj₂ a) → inj₂ (f a)
instance _ = Applicative-ErrorT
Monad-ErrorT : ⦃ _ : Monad M ⦄ → Monad (ErrorT E M)
Monad-ErrorT .return a = return (inj₂ a)
Monad-ErrorT ._>>=_ x f = x >>= λ where
(inj₁ e) → return (inj₁ e)
(inj₂ a) → f a
instance _ = Monad-ErrorT
MonadError-ErrorT : ⦃ _ : Monad M ⦄ → MonadError E (ErrorT E M)
MonadError-ErrorT .error e = return (inj₁ e)
MonadError-ErrorT .catch x h = x >>= Sum.[ h , return ]