module Data.Maybe.Base where

open import Prim.Data.Maybe public

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

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