use for and rfor as primitive Foldable fields

Stdlib/Trait/Foldable/Monomorphic.juvix

@@ -6,8 +6,16 @@ import Stdlib.Trait.Foldable.Polymorphic as Poly;
 --- A trait for combining elements into a single result, processing one element at a time.
 trait
 type Foldable (container elem : Type) :=
-  mkFoldable {-- Combine the elements of the type using the provided function starting with the element in the left-most position.
-  foldl : {B : Type} -> (B -> elem -> B) -> B -> container -> B};
+  mkFoldable {
+    -- Combine the elements of the type using the provided function starting with the element in the left-most position.
+    syntax iterator for {init := 1; range := 1};
+    {-# inline: 0 #-}
+    for : {B : Type} -> (B -> elem -> B) -> B -> container -> B;
+
+    syntax iterator rfor {init := 1; range := 1};
+    {-# inline: 0 #-}
+    rfor : {B : Type} -> (B -> elem -> B) -> B → container → B
+  };
 
 open Foldable;
 
@@ -16,29 +24,23 @@ open Foldable;
 fromPolymorphicFoldable
   {f : Type -> Type} {{foldable : Poly.Foldable f}} {elem} : Foldable (f elem) elem :=
   mkFoldable@{
-    foldl : {B : Type} -> (B -> elem -> B) -> B -> f elem -> B := Poly.foldl
+    for := Poly.for;
+    rfor := Poly.rfor
   };
 
+foldl
+  {container elem}
+  {{Foldable container elem}}
+  {B : Type}
+  (g : B -> elem -> B)
+  (ini : B)
+  (ls : container)
+  : B := for (acc := ini) (x in ls) {g acc x};
+
 --- Combine the elements of the type using the provided function starting with the element in the right-most position.
 foldr
   {container elem : Type}
   {{Foldable container elem}}
   {B : Type}
   (g : elem -> B -> B)
   : B -> container -> B := foldl (flip g);
-
-syntax iterator for {init := 1; range := 1};
-
-{-# inline: 0 #-}
-for
-  {container elem : Type}
-  {B}
-  {{Foldable container elem}}
-  : (B -> elem -> B) -> B -> container -> B := foldl;
-
-syntax iterator rfor {init := 1; range := 1};
-
-{-# inline: 0 #-}
-rfor
-  {container elem : Type} {B} {{Foldable container elem}} (i : B → elem → B) : B → container → B :=
-  foldr (flip i);

Stdlib/Trait/Foldable/Polymorphic.juvix

@@ -5,21 +5,23 @@ import Stdlib.Function open;
 --- A trait for combining elements into a single result, processing one element at a time.
 trait
 type Foldable (f : Type -> Type) :=
-  mkFoldable {-- Combine the elements of the type using the provided function starting with the element in the left-most position.
-  foldl : {A B : Type} -> (B -> A -> B) -> B -> f A -> B};
+  mkFoldable {
+    -- Combine the elements of the type using the provided function starting with the element in the left-most position.
+    syntax iterator for {init := 1; range := 1};
+    {-# inline: 0 #-}
+    for : {A B : Type} -> (B -> A -> B) -> B -> f A -> B;
+
+    syntax iterator rfor {init := 1; range := 1};
+    {-# inline: 0 #-}
+    rfor : {A B : Type} -> (B → A → B) -> B → f A → B
+  };
 
 open Foldable public;
 
 --- Combine the elements of the type using the provided function starting with the element in the right-most position.
-foldr {f : Type -> Type} {{Foldable f}} {A B : Type} (g : A -> B -> B) : B -> f A -> B :=
-  foldl (flip g);
-
-syntax iterator for {init := 1; range := 1};
-
-{-# inline: 0 #-}
-for {f : Type -> Type} {A B} {{Foldable f}} : (B -> A -> B) -> B -> f A -> B := foldl;
+foldl {f : Type -> Type} {{Foldable f}} {A B : Type} (g : B -> A -> B) (ini : B) (ls : f A) : B :=
+  for (acc := ini) (x in ls) {g acc x};
 
-syntax iterator rfor {init := 1; range := 1};
-
-{-# inline: 0 #-}
-rfor {f : Type -> Type} {A B} {{Foldable f}} (i : B → A → B) : B → f A → B := foldr (flip i);
+--- Combine the elements of the type using the provided function starting with the element in the right-most position.
+foldr {f : Type -> Type} {{Foldable f}} {A B : Type} (g : A -> B -> B) (ini : B) (ls : f A) : B :=
+  rfor (acc := ini) (x in ls) {g x acc};