From 4a2261630562fbe60f8655afb696534c2f28a233 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 22 Jul 2024 19:39:19 +0200
Subject: [PATCH] add list instances

---
 Stdlib/Data/List.juvix                 | 10 ++++++++++
 Stdlib/Data/List/Base.juvix            | 10 +++++-----
 Stdlib/Trait/Functor/Monomorphic.juvix |  6 +++++-
 Stdlib/Trait/Functor/Polymorphic.juvix |  8 ++++++--
 4 files changed, 26 insertions(+), 8 deletions(-)

diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix
index 67128654..732af9ca 100644
--- a/Stdlib/Data/List.juvix
+++ b/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;
diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix
index ff3ab015..5b9558ca 100644
--- a/Stdlib/Data/List/Base.juvix
+++ b/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);
diff --git a/Stdlib/Trait/Functor/Monomorphic.juvix b/Stdlib/Trait/Functor/Monomorphic.juvix
index b9aa0ca9..06f6f7f8 100644
--- a/Stdlib/Trait/Functor/Monomorphic.juvix
+++ b/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;
 
diff --git a/Stdlib/Trait/Functor/Polymorphic.juvix b/Stdlib/Trait/Functor/Polymorphic.juvix
index 52c70719..285c904d 100644
--- a/Stdlib/Trait/Functor/Polymorphic.juvix
+++ b/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;