open import 1Lab.Type

open import Meta.Idiom
open import Meta.Bind
open import Meta.Alt

module Data.Maybe.Base where

open import Prim.Data.Maybe public

The Maybe typeπŸ”—

private variable
  β„“ β„“β€² : Level
  A B C : Type β„“

map : (A β†’ B) β†’ Maybe A β†’ Maybe B
map f (just x) = just (f x)
map f nothing  = nothing

extend : Maybe A β†’ (A β†’ Maybe B) β†’ Maybe B
extend (just x) k = k x
extend nothing k  = nothing

instance
  Map-Maybe : Map (eff Maybe)
  Map-Maybe .Map._<$>_ = map

  Idiom-Maybe : Idiom (eff Maybe)
  Idiom-Maybe .Idiom.pure = just
  Idiom-Maybe .Idiom._<*>_ = Ξ» where
    (just f) (just x) β†’ just (f x)
    _ _ β†’ nothing

  Bind-Maybe : Bind (eff Maybe)
  Bind-Maybe .Bind._>>=_ = extend

Pointed types as Maybe-algebrasπŸ”—

maybeβ†’alt : βˆ€ {M : Effect} {β„“} {A : Type β„“}
          β†’ ⦃ _ : Alt M ⦄ ⦃ _ : Idiom M ⦄ β†’ Maybe A β†’ M .Effect.β‚€ A
maybe→alt (just x) = pure x
maybe→alt nothing  = fail