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