add maybe instance

Stdlib/Data/Maybe.juvix

@@ -5,6 +5,7 @@ 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.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
@@ -35,3 +36,14 @@ ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
       | 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;

Stdlib/Trait.juvix

@@ -3,6 +3,7 @@ module Stdlib.Trait;
 import Stdlib.Trait.Eq as Eq open using {Eq; module Eq} public;
 import Stdlib.Trait.Show as Show open using {Show; module Show} public;
 import Stdlib.Trait.Ord as Ord open using {Ord; module Ord} public;
+import Stdlib.Trait.Functor open public;
 import Stdlib.Trait.Partial open public;
 import Stdlib.Trait.Natural open public;
 import Stdlib.Trait.Integral open public;

Stdlib/Trait/Functor.juvix

@@ -2,3 +2,4 @@ module Stdlib.Trait.Functor;
 
 import Stdlib.Trait.Functor.Polymorphic open public;
 import Stdlib.Trait.Functor.Monomorphic as Monomorphic public;
+import Stdlib.Trait.Functor.Monomorphic open using {fromPolymorphicFunctor} public;

Stdlib/Trait/Functor/Monomorphic.juvix

@@ -2,6 +2,7 @@ module Stdlib.Trait.Functor.Monomorphic;
 
 import Stdlib.Data.Fixity open;
 import Stdlib.Data.Unit open;
+import Stdlib.Trait.Functor.Polymorphic as Poly;
 
 trait
 type Functor (container elem : Type) := mkFunctor {map : (elem -> elem) -> container -> container};
@@ -10,8 +11,14 @@ open Functor public;
 
 open Functor public;
 
+fromPolymorphicFunctor {f : Type -> Type} {{Poly.Functor f}} {elem} : Functor (f elem) elem :=
+  mkFunctor@{
+    map := Poly.map
+  };
+
 syntax operator <$> lapp;
 syntax alias <$> := map;
 
 syntax operator $> lapp;
-$> {container elem : Type} {{Functor container elem}} (fa : container) (b : elem) : container := λ {_ := b} <$> fa;
+$> {container elem : Type} {{Functor container elem}} (fa : container) (b : elem) : container :=
+  λ {_ := b} <$> fa;