On Thu, Jul 31, 2014 at 3:33 PM, David Feuer
-- The foldr/cons rule looks nice, but it can give disastrously -- bloated code when commpiling -- array (a,b) [(1,2), (2,2), (3,2), ...very long list... ] -- i.e. when there are very very long literal lists -- So I've disabled it for now. We could have special cases -- for short lists, I suppose. -- "foldr/cons" forall k z x xs. foldr k z (x:xs) = k x (foldr k z xs)
Yes, the foldr/cons rule is a bad idea. However, the cons/build rule should be fine. Both rules have the goal of reducing foldr/cons/build. The problem shows up when we don't have that full pattern. The failure mode of foldr/cons is ridiculously bloated code when the list doesn't end in a build. I can't really think of a failure mode for cons/build. When there's no foldr to cancel with, the build will be inlined; thus, the original (x : build g) which became build(\c n -> c x (g c n)) will then become (x : g (:) []) in the end. If we did not have the cons/build rule, then inlining of build would transform the original (x : build g) into (x : g (:) []) directly. So having the rule, or not, doesn't change the end result. In both cases we might complain that g(:)[] is too slow, but then in both cases we'd expect there to be a g-specific rule for rewriting g(:)[] into some g'. The other possibility for a failure mode would be when there *is* a foldr to cancel with but the cons function is really large— since the cons/build rule duplicates the use of the cons function. That is, we may worry about code like (foldr c0 n0 (x1:x2....:xN : build g)) where N is large. However, note that after applying cons/build repeatedly and then applying foldr/build, we end up with the code ((\c n -> c x1 (c x2 (... (c xN (g c n))...))) c0 n0) —that is, the rules produce a beta-redex, they do not perform the substitution themselves. Since beta-reduction is not performed by rewrite rules, the beta-reducer already has to handle the issue of duplication. -- Live well, ~wren