123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108-------------------------------------------------------------------------- The Agda standard library---- An effectful view of Maybe------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Maybe.Effectful where open import Levelopen import Data.Maybe.Base open import Effect.Choiceopen import Effect.Emptyopen import Effect.Functoropen import Effect.Applicativeopen import Effect.Monad open import Function.Base private variable a b f g m n : Level A : Set a B : Set b -------------------------------------------------------------------------- Maybe applicative functor functor : RawFunctor {f} Maybefunctor = record { _<$>_ = map } applicative : RawApplicative {f} Maybeapplicative = record { rawFunctor = functor ; pure = just ; _<*>_ = maybe map (const nothing) } empty : RawEmpty {f} Maybeempty = record { empty = nothing } choice : RawChoice {f} Maybechoice = record { _<|>_ = _<∣>_ } applicativeZero : RawApplicativeZero {f} MaybeapplicativeZero = record { rawApplicative = applicative ; rawEmpty = empty } alternative : RawAlternative {f} Maybealternative = record { rawApplicativeZero = applicativeZero ; rawChoice = choice } -------------------------------------------------------------------------- Maybe monad monad : RawMonad {f} Maybemonad = record { rawApplicative = applicative ; _>>=_ = _>>=_ } join : Maybe (Maybe A) → Maybe Ajoin = Join.join monad monadZero : RawMonadZero {f} MaybemonadZero = record { rawMonad = monad ; rawEmpty = empty } monadPlus : RawMonadPlus {f} MaybemonadPlus {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 )