------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of Maybe
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Maybe.Effectful.Transformer where
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe)
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad; RawMonadT)
open import Function.Base using (_∘′_; _$_)
open import Level using (Level; _⊔_)
private
variable
f g : Level
M : Set f → Set g
------------------------------------------------------------------------
-- Maybe monad transformer
record MaybeT (M : Set f → Set g) (A : Set f) : Set g where
constructor mkMaybeT
field runMaybeT : M (Maybe A)
open MaybeT public
------------------------------------------------------------------------
-- Structure
functor : RawFunctor M → RawFunctor {f} (MaybeT M)
functor M = record
{ _<$>_ = λ f → mkMaybeT ∘′ (Maybe.map f <$>_) ∘′ runMaybeT
} where open RawFunctor M
applicative : RawApplicative M → RawApplicative {f} (MaybeT M)
applicative M = record
{ rawFunctor = functor rawFunctor
; pure = mkMaybeT ∘′ pure ∘′ just
; _<*>_ = λ mf ma → mkMaybeT (Maybe.ap <$> runMaybeT mf <*> runMaybeT ma)
} where open RawApplicative M
monad : RawMonad M → RawMonad {f} (MaybeT M)
monad M = record
{ rawApplicative = applicative rawApplicative
; _>>=_ = λ ma f → mkMaybeT $ do
a ← runMaybeT ma
maybe (runMaybeT ∘′ f) (pure nothing) a
} where open RawMonad M
monadT : RawMonadT {f} {g} MaybeT
monadT {M = F} M = record
{ lift = mkMaybeT ∘′ (just <$>_)
; 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