------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of Maybe
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Maybe.Effectful where
open import Data.Maybe.Base using (Maybe; just; nothing; map; _>>=_; _<∣>_; maybe)
open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Functor using (RawFunctor)
open import Effect.Monad
open import Function.Base using (flip; const; _∘_)
open import Level using (Level; _⊔_)
private
variable
a b f g m n : Level
A : Set a
B : Set b
------------------------------------------------------------------------
-- Maybe applicative functor
functor : RawFunctor {f} Maybe
functor = record
{ _<$>_ = map
}
applicative : RawApplicative {f} Maybe
applicative = record
{ rawFunctor = functor
; pure = just
; _<*>_ = maybe map (const nothing)
}
empty : RawEmpty {f} Maybe
empty = record { empty = nothing }
choice : RawChoice {f} Maybe
choice = record { _<|>_ = _<∣>_ }
applicativeZero : RawApplicativeZero {f} Maybe
applicativeZero = record
{ rawApplicative = applicative
; rawEmpty = empty
}
alternative : RawAlternative {f} Maybe
alternative = record
{ rawApplicativeZero = applicativeZero
; rawChoice = choice
}
------------------------------------------------------------------------
-- Maybe monad
monad : RawMonad {f} Maybe
monad = record
{ rawApplicative = applicative
; _>>=_ = _>>=_
}
join : Maybe (Maybe A) → Maybe A
join = Join.join monad
monadZero : RawMonadZero {f} Maybe
monadZero = record
{ rawMonad = monad
; rawEmpty = empty
}
monadPlus : RawMonadPlus {f} Maybe
monadPlus {f} = record
{ rawMonadZero = monadZero
; rawChoice = choice
}
module TraversableA {F} (App : RawApplicative {f} {g} F) where
open RawApplicative App
sequenceA : Maybe (F A) → F (Maybe A)
sequenceA nothing = pure nothing
sequenceA (just x) = just <$> x
mapA : (A → F B) → Maybe A → F (Maybe B)
mapA f = sequenceA ∘ map f
forA : Maybe A → (A → F B) → F (Maybe B)
forA = flip mapA
module TraversableM {M} (Mon : RawMonad {m} {n} 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