------------------------------------------------------------------------ -- The Agda standard library -- -- The Maybe type and some operations ------------------------------------------------------------------------ -- The definitions in this file are reexported by Data.Maybe. {-# OPTIONS --without-K --safe #-} module Data.Maybe.Base where open import Level open import Data.Bool.Base using (Bool; true; false; not) open import Data.Unit.Base using (⊤) open import Data.These.Base using (These; this; that; these) open import Data.Product as Prod using (_×_; _,_) open import Function.Base open import Relation.Nullary.Reflects open import Relation.Nullary private variable a b c : Level A : Set a B : Set b C : Set c ------------------------------------------------------------------------ -- Definition open import Agda.Builtin.Maybe public using (Maybe; just; nothing) ------------------------------------------------------------------------ -- Some operations boolToMaybe : Bool → Maybe ⊤ boolToMaybe true = just _ boolToMaybe false = nothing is-just : Maybe A → Bool is-just (just _) = true is-just nothing = false is-nothing : Maybe A → Bool is-nothing = not ∘ is-just decToMaybe : Dec A → Maybe A decToMaybe ( true because [a]) = just (invert [a]) decToMaybe (false because _ ) = nothing -- A dependent eliminator. maybe : ∀ {A : Set a} {B : Maybe A → Set b} → ((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x maybe j n (just x) = j x maybe j n nothing = n -- A non-dependent eliminator. maybe′ : (A → B) → B → Maybe A → B maybe′ = maybe -- A defaulting mechanism fromMaybe : A → Maybe A → A fromMaybe = maybe′ id -- A safe variant of "fromJust". If the value is nothing, then the -- return type is the unit type. module _ {a} {A : Set a} where From-just : Maybe A → Set a From-just (just _) = A From-just nothing = Lift a ⊤ from-just : (x : Maybe A) → From-just x from-just (just x) = x from-just nothing = _ -- Functoriality: map map : (A → B) → Maybe A → Maybe B map f = maybe (just ∘ f) nothing -- Applicative: ap ap : Maybe (A → B) → Maybe A → Maybe B ap nothing = const nothing ap (just f) = map f -- Monad: bind infixl 1 _>>=_ _>>=_ : Maybe A → (A → Maybe B) → Maybe B nothing >>= f = nothing just a >>= f = f a -- Alternative: <∣> _<∣>_ : Maybe A → Maybe A → Maybe A just x <∣> my = just x nothing <∣> my = my -- Just when the boolean is true when : Bool → A → Maybe A when b c = map (const c) (boolToMaybe b) ------------------------------------------------------------------------ -- Aligning and zipping alignWith : (These A B → C) → Maybe A → Maybe B → Maybe C alignWith f (just a) (just b) = just (f (these a b)) alignWith f (just a) nothing = just (f (this a)) alignWith f nothing (just b) = just (f (that b)) alignWith f nothing nothing = nothing zipWith : (A → B → C) → Maybe A → Maybe B → Maybe C zipWith f (just a) (just b) = just (f a b) zipWith _ _ _ = nothing align : Maybe A → Maybe B → Maybe (These A B) align = alignWith id zip : Maybe A → Maybe B → Maybe (A × B) zip = zipWith _,_ ------------------------------------------------------------------------ -- Injections. thisM : A → Maybe B → These A B thisM a = maybe′ (these a) (this a) thatM : Maybe A → B → These A B thatM = maybe′ these that