------------------------------------------------------------------------
-- The Agda standard library
--
-- The error monad transformer
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Level using (Level; _⊔_; suc)
module Effect.Monad.Error.Transformer {e} (E : Set e) (a : Level) where
open import Effect.Monad using (RawMonad)
open import Function.Base using (_∘′_; _$_)
private
variable
f ℓ : Level
A B : Set ℓ
M : Set f → Set ℓ
------------------------------------------------------------------------
-- Error monad operations
record RawMonadError
(M : Set (e ⊔ a) → Set ℓ)
: Set (suc (e ⊔ a) ⊔ ℓ) where
field
throw : E → M A
catch : M A → (E → M A) → M A
during : (E → E) → M A → M A
during f ma = catch ma (throw ∘′ f)
------------------------------------------------------------------------
-- Monad error transformer specifics
module Sumₗ where
open import Data.Sum.Base using (inj₁; inj₂; [_,_]′)
open import Data.Sum.Effectful.Left.Transformer E a
monadError : RawMonad M → RawMonadError (SumₗT M)
monadError M = record
{ throw = mkSumₗT ∘′ pure ∘′ inj₁
; catch = λ ma k → mkSumₗT $ do
a ← runSumₗT ma
[ runSumₗT ∘′ k , pure ∘′ inj₂ ]′ a
} where open RawMonad M
module Sumᵣ where
open import Data.Sum.Base using (inj₁; inj₂; [_,_]′)
open import Data.Sum.Effectful.Right.Transformer a E
monadError : RawMonad M → RawMonadError (SumᵣT M)
monadError M = record
{ throw = mkSumᵣT ∘′ pure ∘′ inj₂
; catch = λ ma k → mkSumᵣT $ do
a ← runSumᵣT ma
[ pure ∘′ inj₁ , runSumᵣT ∘′ k ]′ a
} where open RawMonad M
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4