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