-
Notifications
You must be signed in to change notification settings - Fork 380
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[ base ] Change how folds are defined for Data.Vect
#2707
base: main
Are you sure you want to change the base?
Conversation
* Adds dependent folds, where the type of the accumulator depends on the current length of the `Vect`. * Changes the `Foldable` instance for `Vect` to be expressed via the former. * Moves the tail-recursive version of `foldr` to a separate function, `foldrTR`. * As a sanity check, proves that `foldrTR` is equal to `foldr`. * Changes the definition of `sumR` in `Data.Vect.Properties.Foldr` to accept just `Vect`s, since other foldables might define `foldr` differently, and this function lives in a module with `Vect` in name anyway.
We have to be very careful about this, as it looks like it shows quadratic runtime complexity due to #2166. For instance, if I run the following program on my machine with an argument of "100000", it takes 5 seconds (!) to finish: module Foldl
import Data.Vect
import System
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
fold : (acc -> e -> acc) -> acc -> Vect n e -> acc
fold f acc xs = foldlD (const _) f acc xs
main : IO ()
main = do
[_,s] <- getArgs | _ => die "Invalid number of args"
printLn $ fold (+) Z (replicate (cast s) 1) If I replace |
Two more data points: The following, which uses a trick described in #2166 by using a function with an explicit erased argument, does not work here: foldlDImpl : (0 accTy : Nat -> Type) ->
(f : (0 k : Nat) -> accTy k -> a -> accTy (S k)) ->
(acc : accTy Z) ->
(xs : Vect n a) ->
accTy n
foldlDImpl _ _ acc [] = acc
foldlDImpl accTy f acc (x :: xs) = foldlDImpl (accTy . S) (\k => f (S k)) (f _ acc x) xs The only way I got this to run in linear time is by means of foldlDImpl : (0 accTy : Nat -> Type) ->
(f : (0 k : Nat) -> accTy k -> a -> accTy (S k)) ->
(acc : accTy Z) ->
(xs : Vect n a) ->
accTy n
foldlDImpl _ _ acc [] = acc
foldlDImpl accTy f acc (x :: xs) = foldlDImpl (accTy . S) (believe_me f) (f _ acc x) xs
foldlD : (0 accTy : Nat -> Type) ->
(f : forall k. accTy k -> a -> accTy (S k)) ->
(acc : accTy Z) ->
(xs : Vect n a) ->
accTy n
foldlD at f = foldlDImpl at $ \_ => f |
OK, I got a O(n) version without foldlD : (0 accTy : Nat -> Type) ->
(f : forall k. accTy k -> a -> accTy (S k)) ->
(acc : accTy Z) ->
(xs : Vect n a) ->
accTy n
foldlD at f acc xs = go acc xs
where go : at k -> Vect m a -> at (k + m)
go x [] =
rewrite plusZeroRightNeutral k in x
go {m = S l} x (y :: xs) =
rewrite sym (plusSuccRightSucc k l) in go (f x y) xs |
Interesting, thanks for looking into this! Since I'll eventually need to prove things about functions expressed with
Personally, I'd vote for (2), as it seems like a fair share of proofs about What do you think? |
The whole point of this refactoring is that the |
Vect
.Foldable
instance forVect
to be expressed via the former.foldr
to a separate function,foldrTR
.foldrTR
is equal tofoldr
.sumR
inData.Vect.Properties.Foldr
to accept justVect
s, since other foldables might definefoldr
differently, and this function lives in a module withVect
in name anyway.