add list instances

Stdlib/Data/List.juvix

@@ -7,6 +7,7 @@ import Stdlib.Data.String.Base open;
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
+import Stdlib.Trait.Functor as Functorr open;
 import Stdlib.Trait.Partial open;
 
 --- 𝒪(1). Partial function that returns the first element of a ;List;.
@@ -49,3 +50,12 @@ showListI {A} {{Show A}} : Show (List A) :=
       | nil := "nil"
       | s := "(" ++str go s ++str ")"
     };
+
+instance
+functorListI : Functor List :=
+  mkFunctor@{
+    map := listMap
+  };
+
+instance
+monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A := fromPolymorphicFunctor;

Stdlib/Data/List/Base.juvix

@@ -50,13 +50,13 @@ syntax iterator for {init := 1; range := 1};
 {-# inline: 0, isabelle-function: {name: "foldl"} #-}
 for : {A B : Type} → (B → A → B) → B → List A → B := foldl;
 
-syntax iterator map {init := 0; range := 1};
+syntax iterator listMap {init := 0; range := 1};
 
 --- 𝒪(𝓃). Maps a function over each element of a ;List;.
 {-# specialize: [1] #-}
-map {A B} (f : A → B) : List A → List B
+listMap {A B} (f : A → B) : List A → List B
   | nil := nil
-  | (h :: hs) := f h :: map f hs;
+  | (h :: hs) := f h :: listMap f hs;
 
 syntax iterator filter {init := 0; range := 1};
 
@@ -221,10 +221,10 @@ syntax iterator concatMap {init := 0; range := 1};
 
 --- Applies a function to every item on a ;List; and concatenates the result.
 --- 𝒪(𝓃), where 𝓃 is the number of items in the resulting list.
-concatMap {A B} (f : A -> List B) : List A -> List B := map f >> flatten;
+concatMap {A B} (f : A -> List B) : List A -> List B := listMap f >> flatten;
 
 --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix.
 transpose {A} : List (List A) -> List (List A)
   | nil := nil
-  | (xs :: nil) := map λ {x := x :: nil} xs
+  | (xs :: nil) := listMap λ {x := x :: nil} xs
   | (xs :: xss) := zipWith (::) xs (transpose xss);

Stdlib/Trait/Functor/Monomorphic.juvix

@@ -5,7 +5,11 @@ import Stdlib.Data.Unit open;
 import Stdlib.Trait.Functor.Polymorphic as Poly;
 
 trait
-type Functor (container elem : Type) := mkFunctor {map : (elem -> elem) -> container -> container};
+type Functor (container elem : Type) :=
+  mkFunctor {
+    syntax iterator map {init := 0; range := 1};
+    map : (elem -> elem) -> container -> container
+  };
 
 open Functor public;
 

Stdlib/Trait/Functor/Polymorphic.juvix

@@ -4,14 +4,18 @@ import Stdlib.Data.Fixity open;
 import Stdlib.Data.Unit open;
 
 trait
-type Functor (f : Type -> Type) := mkFunctor {map : {A B : Type} -> (A -> B) -> f A -> f B};
+type Functor (f : Type -> Type) :=
+  mkFunctor {
+    syntax iterator map {init := 0; range := 1};
+    map : {A B : Type} -> (A -> B) -> f A -> f B
+  };
 
 open Functor public;
 
 open Functor public;
 
 syntax operator <$> lapp;
-syntax alias <$> := map;
+<$> {f : Type -> Type} {{Functor f}} {A B} (fun : A -> B) (l : f A) : f B := map fun l;
 
 syntax operator $> lapp;
 $> {f : Type → Type} {A B : Type} {{Functor f}} (fa : f A) (b : B) : f B := λ {_ := b} <$> fa;