    ------------------------------------------------------------------------
    -- 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