[ base ] Change how folds are defined for Data.Vect

libs/base/Data/Vect.idr

@@ -377,19 +377,41 @@ mapMaybe f (x::xs) =
        Nothing => (  len **      ys)
 
 --------------------------------------------------------------------------------
--- Folds
+-- Dependent folds
 --------------------------------------------------------------------------------
 
-public export
-foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
-foldrImpl f e go [] = go e
-foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
+||| Dependent right fold.
+|||
+||| Use this instead of `Foldable`'s `foldr`
+||| if your accumulator type depends on the length of the `Vect`.
+foldrD : (0 accTy : Nat -> Type) ->
+         (f : forall k. a -> accTy k -> accTy (S k)) ->
+         (acc : accTy Z) ->
+         (xs : Vect n a) ->
+         accTy n
+foldrD _     _ acc []        = acc
+foldrD accTy f acc (x :: xs) = f x (foldrD accTy f acc xs)
+
+||| Dependent left fold.
+|||
+||| Use this instead of `Foldable`'s `foldl`
+||| if your accumulator type depends on the length of the `Vect`.
+foldlD : (0 accTy : Nat -> Type) ->
+         (f : forall k. accTy k -> a -> accTy (S k)) ->
+         (acc : accTy Z) ->
+         (xs : Vect n a) ->
+         accTy n
+foldlD _     _ acc []        = acc
+foldlD accTy f acc (x :: xs) = foldlD (accTy . S) f (acc `f` x) xs
+
+--------------------------------------------------------------------------------
+-- Folds
+--------------------------------------------------------------------------------
 
 public export
 implementation Foldable (Vect n) where
-  foldr f e xs = foldrImpl f e id xs
-  foldl f z [] = z
-  foldl f z (x :: xs) = foldl f (f z x) xs
+  foldr f acc xs = foldrD (const _) f acc xs
+  foldl f acc xs = foldlD (const _) f acc xs
 
   null [] = True
   null _ = False
@@ -400,6 +422,40 @@ implementation Foldable (Vect n) where
 -- Special folds
 --------------------------------------------------------------------------------
 
+||| Tail-recursive right fold
+|||
+||| Depending on the accumulator, codegen backend and what not,
+||| it might be more efficient than plain `foldr`.
+
+public export
+foldrImpl : (a -> acc -> acc) -> acc -> (acc -> acc) -> Vect n a -> acc
+foldrImpl f e go [] = go e
+foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
+
+public export
+foldrTR : (a -> acc -> acc) -> acc -> Vect n a -> acc
+foldrTR f e xs = foldrImpl f e id xs
+
+export
+foldrImplStep : (f : a -> accTy -> accTy) ->
+                (g : accTy -> accTy) ->
+                (acc : accTy) ->
+                (x : a) ->
+                (xs : Vect n a) ->
+                f x (foldrImpl f acc g xs) = foldrImpl f acc (f x . g) xs
+foldrImplStep f g acc x [] = Refl
+foldrImplStep f g acc x (x' :: xs) = foldrImplStep f (g . f x') acc x xs
+
+export
+foldrTRisFoldr : (f : a -> accTy -> accTy) ->
+                 (acc : accTy) ->
+                 (xs : Vect n a) ->
+                 foldr f acc xs = foldrTR f acc xs
+foldrTRisFoldr f acc [] = Refl
+foldrTRisFoldr f acc (x :: xs) = rewrite foldrTRisFoldr f acc xs in
+                                         foldrImplStep f id acc x xs
+
+
 ||| Flatten a vector of equal-length vectors
 |||
 ||| ```idris example

libs/contrib/Data/Vect/Properties/Foldr.idr

@@ -1,13 +1,13 @@
 |||
 |||
-||| foldr is the unique solution to the equation:
+||| foldrTR is the unique solution to the equation:
 |||
 |||   h f e [] = e
-|||   h f e (x :: xs) = x `h` (foldr f e xs)
+|||   h f e (x :: xs) = x `h` (foldrTR f e xs)
 |||
 ||| (This fact is called 'the universal property of foldr'.)
 |||
-||| Since the prelude defines foldr tail-recursively, this fact isn't immediate
+||| Since the prelude defines foldrTR tail-recursively, this fact isn't immediate
 ||| and we need some lemmata to prove it.
 module Data.Vect.Properties.Foldr
 
@@ -19,10 +19,10 @@ import Data.Nat
 import Syntax.PreorderReasoning
 import Syntax.PreorderReasoning.Generic
 
-||| Sum implemented with foldr
+||| Sum implemented with the tail-recursive foldr
 public export
-sumR : Num a => Foldable f => f a -> a
-sumR = foldr (+) 0
+sumR : Num a => Vect n a -> a
+sumR = foldrTR (+) 0
 
 %transform "sumR/sum" sumR = sum
 
@@ -71,24 +71,24 @@ foldrImplNaturality : (f : a -> b -> b) -> (e : b) -> (xs : Vect n a) -> (go1, g
 foldrImplNaturality f e    []     go1 go2 = Refl
 foldrImplNaturality f e (x :: xs) go1 go2 = foldrImplNaturality f e xs go1 (go2 . (f x))
 
-||| Our tail-recursive foldr preserves the vector structure
+||| Our tail-recursive foldrTR preserves the vector structure
 export
-foldrVectHomomorphism : VectHomomorphismProperty f e (foldr f e)
+foldrVectHomomorphism : VectHomomorphismProperty f e (foldrTR f e)
 foldrVectHomomorphism = ShowVectHomomorphismProperty
   { nil  = Refl
   , cons = \x, xs => Calc $
-    |~ foldr f e (x :: xs)
+    |~ foldrTR f e (x :: xs)
     ~~ foldrImpl f e (id . (f x)) xs ...(Refl)
     ~~ foldrImpl f e ((f x) . id) xs ...(foldrImplExtensional f e _ _ (\y => Refl) xs)
     ~~ f x (foldrImpl f e id xs)     ...(foldrImplNaturality f e xs (f x) _)
-    ~~ f x (foldr f e xs)            ...(Refl)
+    ~~ f x (foldrTR f e xs)          ...(Refl)
   }
 
-||| foldr is the unique function preserving the vector structure
+||| foldrTR is the unique function preserving the vector structure
 export
-foldrUniqueness : (h : forall n . Vect n a -> b) -> VectHomomorphismProperty f e h -> (xs : Vect n a) -> h xs = foldr f e xs
+foldrUniqueness : (h : forall n . Vect n a -> b) -> VectHomomorphismProperty f e h -> (xs : Vect n a) -> h xs = foldrTR f e xs
 foldrUniqueness {f} h prf xs = irrelevantEq $
-  nilConsInitiality f e h (foldr f e) prf foldrVectHomomorphism xs
+  nilConsInitiality f e h (foldrTR f e) prf foldrVectHomomorphism xs
 
 
 ||| Each summand is `LTE` the sum