------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of the Sum type (Right-biased)
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Level
module Data.Sum.Effectful.Right.Transformer (a : Level) {b} (B : Set b) where
open import Data.Sum.Base
open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Function.Base
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.Right a B using (Sumᵣ)
------------------------------------------------------------------------
-- Right-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 ([ map₁ , const ∘′ inj₂ ]′ <$> runSumᵣT mf <*> runSumᵣT mx)
} where open RawApplicative M
empty : RawApplicative M → B → 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 ([ const ∘ inj₁ , flip const ]′ <$> runSumᵣT ma₁ <*> runSumᵣT ma₁)
} where open RawApplicative M
applicativeZero : RawApplicative M → B → RawApplicativeZero (SumᵣT M)
applicativeZero M a = record
{ rawApplicative = applicative M
; rawEmpty = empty M a
}
alternative : RawApplicative M → B → 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
[ runSumᵣT ∘′ f , pure ∘′ inj₂ ]′ 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