module Prelude.Maybe import Builtins import Prelude.Algebra import Prelude.Basics import Prelude.Bool import Prelude.Cast import Prelude.Classes import Prelude.Foldable %access public %default total ||| An optional value. This can be used to represent the possibility of ||| failure, where a function may return a value, or not. data Maybe a = ||| No value stored Nothing | ||| A value of type `a` is stored Just a -------------------------------------------------------------------------------- -- Syntactic tests -------------------------------------------------------------------------------- isNothing : Maybe a -> Bool isNothing Nothing = True isNothing (Just j) = False isJust : Maybe a -> Bool isJust Nothing = False isJust (Just j) = True ||| Proof that some `Maybe` is actually `Just` data IsJust : Maybe a -> Type where ItIsJust : IsJust (Just x) -------------------------------------------------------------------------------- -- Misc -------------------------------------------------------------------------------- maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b maybe n j Nothing = n maybe n j (Just x) = (Force j) x ||| Convert a `Maybe a` value to an `a` value by providing a default `a` value ||| in the case that the `Maybe` value is `Nothing`. fromMaybe : (Lazy a) -> Maybe a -> a fromMaybe def Nothing = def fromMaybe def (Just j) = j ||| Returns `Just` the given value if the conditional is `True` ||| and `Nothing` if the conditional is `False`. toMaybe : Bool -> Lazy a -> Maybe a toMaybe True j = Just j toMaybe False j = Nothing justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y justInjective Refl = Refl ||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case ||| that the `Maybe` value is `Nothing`. lowerMaybe : Monoid a => Maybe a -> a lowerMaybe Nothing = neutral lowerMaybe (Just x) = x ||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise. raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a raiseToMaybe x = if x == neutral then Nothing else Just x -------------------------------------------------------------------------------- -- Class instances -------------------------------------------------------------------------------- maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b maybe_bind Nothing k = Nothing maybe_bind (Just x) k = k x instance (Eq a) => Eq (Maybe a) where Nothing == Nothing = True Nothing == (Just _) = False (Just _) == Nothing = False (Just a) == (Just b) = a == b ||| Prioritised choice. Just like the `Alternative` instance, the ||| `Semigroup` for `Maybe a` keeps the first succeeding computation. ||| ||| **NB**: This is a different choice than in the Haskell libraries. ||| Use `collectJust` to get the Haskell behaviour. instance Semigroup (Maybe a) where Nothing <+> m = m (Just x) <+> _ = Just x ||| Transform any semigroup into a monoid by using `Nothing` as the ||| designated neutral element and collecting the contents of the ||| `Just` constructors using a semigroup structure on `a`. This is ||| the behaviour in the Haskell libraries. instance [collectJust] Semigroup a => Semigroup (Maybe a) where Nothing <+> m = m m <+> Nothing = m (Just m1) <+> (Just m2) = Just (m1 <+> m2) instance Monoid (Maybe a) where neutral = Nothing instance (Monoid a, Eq a) => Cast a (Maybe a) where cast = raiseToMaybe instance (Monoid a) => Cast (Maybe a) a where cast = lowerMaybe instance Foldable Maybe where foldr _ z Nothing = z foldr f z (Just x) = f x z