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;
import Stdlib.Data.Pair.Base open;
deriving instance
eqMaybeI {A} {{Eq A}} : Eq (Maybe A);
instance
showMaybeI {A} {{Show A}} : Show (Maybe A) :=
mkShow@{
show (m : Maybe A) : String :=
case m of
| nothing := "nothing"
| just a := "just " ++str Show.show a;
};
deriving instance
ordMaybeI {A} {{Ord A}} : Ord (Maybe A);
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} (listOfFuns : Maybe (A -> B)) (list : Maybe A) : Maybe B :=
case listOfFuns, list of
| just f, just x := just (f x)
| _, _ := nothing;
};
instance
monadMaybeI : Monad Maybe :=
mkMonad@{
bind {A B} (maybe : Maybe A) (fun : A -> Maybe B) : Maybe B :=
case maybe of
| nothing := nothing
| just a := fun a;
};