------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of the Sum type (Left-biased)
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Level
module Data.Sum.Effectful.Left.Transformer {a} (A : Set a) (b : Level) where
open import Data.Sum.Base using (map₂ ; inj₁ ; inj₂; _⊎_; [_,_]′)
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative
using (RawApplicative; RawApplicativeZero; RawAlternative)
open import Effect.Monad using (RawMonad; RawMonadT)
open import Function.Base using (const; flip; _∘_; _∘′_; _$_)
private
variable
M : Set (a ⊔ b) → Set (a ⊔ b)
-- To minimize the universe level of the RawFunctor, we require that
-- elements of B are "lifted" to a copy of B at a higher universe level
-- (a ⊔ b). See the examples for how this is done.
open import Data.Sum.Effectful.Left A b using (Sumₗ)
------------------------------------------------------------------------
-- Left-biased monad transformer instance for _⊎_
record SumₗT
(M : Set (a ⊔ b) → Set (a ⊔ b))
(B : Set (a ⊔ b)) : Set (a ⊔ b) where
constructor mkSumₗT
field runSumₗT : M (Sumₗ B)
open SumₗT public
------------------------------------------------------------------------
-- Structure
functor : RawFunctor M → RawFunctor (SumₗT M)
functor M = record
{ _<$>_ = λ f → mkSumₗT ∘′ (map₂ f <$>_) ∘′ runSumₗT
} where open RawFunctor M
applicative : RawApplicative M → RawApplicative (SumₗT M)
applicative M = record
{ rawFunctor = functor rawFunctor
; pure = mkSumₗT ∘′ pure ∘′ inj₂
; _<*>_ = λ mf mx → mkSumₗT ([ const ∘′ inj₁ , map₂ ]′ <$> runSumₗT mf <*> runSumₗT mx)
} where open RawApplicative M
empty : RawApplicative M → A → RawEmpty (SumₗT M)
empty M a = record
{ empty = mkSumₗT (pure (inj₁ a))
} where open RawApplicative M
choice : RawApplicative M → RawChoice (SumₗT M)
choice M = record
{ _<|>_ = λ ma₁ ma₂ → mkSumₗT ([ flip const , const ∘ inj₂ ]′ <$> runSumₗT ma₁ <*> runSumₗT ma₂)
} where open RawApplicative M
applicativeZero : RawApplicative M → A → RawApplicativeZero (SumₗT M)
applicativeZero M a = record
{ rawApplicative = applicative M
; rawEmpty = empty M a
}
alternative : RawApplicative M → A → RawAlternative (SumₗT M)
alternative M a = record
{ rawApplicativeZero = applicativeZero M a
; rawChoice = choice M
}
monad : RawMonad M → RawMonad (SumₗT M)
monad M = record
{ rawApplicative = applicative rawApplicative
; _>>=_ = λ ma f → mkSumₗT $ do
a ← runSumₗT ma
[ pure ∘′ inj₁ , runSumₗT ∘′ f ]′ a
} where open RawMonad M
monadT : RawMonadT SumₗT
monadT M = record
{ lift = mkSumₗT ∘′ (inj₂ <$>_)
; rawMonad = monad M
} 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