------------------------------------------------------------------------
-- 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 (a : Level) {b} (B : Set b) where
open import Algebra.Bundles using (RawMonoid)
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; RawMonadZero; RawMonadPlus; module Join)
open import Function.Base using (const; flip; _∘_; _∘′_; _$_; _|>′_)
Sumᵣ : Set (a ⊔ b) → Set (a ⊔ b)
Sumᵣ A = A ⊎ B
functor : RawFunctor Sumᵣ
functor = record { _<$>_ = map₁ }
empty : B → RawEmpty Sumᵣ
empty b = record { empty = inj₂ b }
choice : RawChoice Sumᵣ
choice = record { _<|>_ = [ const ∘′ inj₁ , flip const ]′ }
applicative : RawApplicative Sumᵣ
applicative = record
{ rawFunctor = functor
; pure = inj₁
; _<*>_ = [ map₁ , const ∘ inj₂ ]′
}
applicativeZero : B → RawApplicativeZero Sumᵣ
applicativeZero b = record
{ rawApplicative = applicative
; rawEmpty = empty b
}
alternative : B → RawAlternative Sumᵣ
alternative b = record
{ rawApplicativeZero = applicativeZero b
; rawChoice = choice
}
monad : RawMonad Sumᵣ
monad = record
{ rawApplicative = applicative
; _>>=_ = [ _|>′_ , const ∘′ inj₂ ]′
}
join : {A : Set (a ⊔ b)} → Sumᵣ (Sumᵣ A) → Sumᵣ A
join = Join.join monad
monadZero : B → RawMonadZero Sumᵣ
monadZero b = record
{ rawMonad = monad
; rawEmpty = empty b
}
monadPlus : B → RawMonadPlus Sumᵣ
monadPlus b = record
{ rawMonadZero = monadZero b
; rawChoice = choice
}
------------------------------------------------------------------------
-- Get access to other monadic functions
module TraversableA {F} (App : RawApplicative {a ⊔ b} {a ⊔ b} F) where
open RawApplicative App
sequenceA : ∀ {A} → Sumᵣ (F A) → F (Sumᵣ A)
sequenceA (inj₂ a) = pure (inj₂ a)
sequenceA (inj₁ x) = inj₁ <$> x
mapA : ∀ {A B} → (A → F B) → Sumᵣ A → F (Sumᵣ B)
mapA f = sequenceA ∘ map₁ f
forA : ∀ {A B} → Sumᵣ A → (A → F B) → F (Sumᵣ B)
forA = flip mapA
module TraversableM {M} (Mon : RawMonad {a ⊔ b} {a ⊔ b} M) where
open RawMonad Mon
open TraversableA rawApplicative public
renaming
( sequenceA to sequenceM
; mapA to mapM
; forA to forM
)
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