module Stdlib.Data.Maybe;
import Stdlib.Data.Maybe.Base open public;
import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;
import Stdlib.Trait.Functor open;
import Stdlib.Trait.Applicative open;
import Stdlib.Trait.Monad open;
import Stdlib.Data.Bool.Base open;
import Stdlib.Data.String.Base open;
instance
eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
mkEq
λ {
| nothing nothing := true
| (just a1) (just a2) := Eq.eq a1 a2
| _ _ := false
};
instance
showMaybeI {A} {{Show A}} : Show (Maybe A) :=
mkShow
λ {
| nothing := "nothing"
| (just a) := "just " ++str Show.show a
};
instance
ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
mkOrd
λ {
| nothing nothing := EQ
| (just a1) (just a2) := Ord.cmp a1 a2
| nothing (just _) := LT
| (just _) nothing := GT
};
instance
functorMaybeI : Functor Maybe :=
mkFunctor@{
map {A B} (f : A -> B) : Maybe A -> Maybe B
| nothing := nothing
| (just a) := just (f a)
};
instance
monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A :=
fromPolymorphicFunctor;
instance
applicativeMaybeI : Applicative Maybe :=
mkApplicative@{
pure := just;
ap {A B} : Maybe (A -> B) -> Maybe A -> Maybe B
| (just f) (just x) := just (f x)
| _ _ := nothing
};
instance
monadMaybeI : Monad Maybe :=
mkMonad@{
bind {A B} : Maybe A -> (A -> Maybe B) -> Maybe B
| nothing _ := nothing
| (just a) f := f a
};