Re: [Haskell-cafe] Fold that quits early?

24 Jan 2009

      foldr f z xs =
   x0 `f` (x1 `f` (x2 `f` ... (xN `f` z) ...))

In particular, note that if f is a total function, xs is finite and
totally defined, and z is totally defined, then the result of this
fold is totally defined.

Now consider your "f" (rewritten slightly)

f x xs
   | null xs = []
   | p x = []
   | otherwise = foldr f (x:xs) (g x xs)

with these definitions:

c _ = False
g = (:)

c and g are definitely total functions, so what happens when we
evaluate f 0 [1]?

f 0 [1]
        = foldr f [0,1] [0,1]
        = let t1 = foldr f [0,1] [1] in f 0 $ t1
        = let t1 = foldr f [0,1] [1] in foldr f (0 : t1) (0 : t1)
        = let t1 = foldr f [0,1] [1]
              t2 = foldr f (0:t1) t1
          in f 0 t2

etc.; this is clearly non-terminating.

Therefore there is no way to make f into a fold.

Any errors in my logic?

  -- ryan

2009/1/24 Andrew Wagner :
...
Ahem. That's what happens when you don't type-check your brainstorming
before barfing it out, kids. Sorry about that. Let's try this again:
f _ [] = []
f y x | c y = []
        | otherwise = foldr f (y:x) (g y x)
I've got a fold on the inside now, but I'm pretty sure the whole thing is
just a fold. Not quite there yet, though...
On Sat, Jan 24, 2009 at 1:42 PM, Andrew Wagner 
wrote:
...
Actually, I think I can rewrite it this way:
f xs [] = False
f xs (y:ys) | any c ys' = True
                | otherwise = f (f (y:xs) ys') ys
  where ys' = g y ys
This should help, I think.
On Sat, Jan 24, 2009 at 12:11 PM, Dan Doel  wrote:
...
On Saturday 24 January 2009 11:39:13 am Andrew Wagner wrote:
...
This is almost a fold, but seemingly not quite? I know I've seem some
talk
of folds that potentially "quit" early. but not sure where I saw that,
or
if it fits.
f xs [] = False
f xs (y:ys) | any c ys' = True
| otherwise = f (nub (y:xs)) (ys' ++ ys)
where ys' = g y xs
Quitting early isn't the problem. For instance, any is defined in terms
of
foldr, and it works fine on infinite lists, quitting as soon as it finds
a
True. As long as you don't use the result of the recursive call (which is
the
second argument in the function you pass to foldr), it will exit early.
The problem is that your function doesn't look structurally recursive,
and
that's what folds (the usual ones, anyway) are: a combinator for
structural
recursion. The problem is in your inductive case, where you don't just
recurse
on "ys", you instead recurse on "ys' ++ ys", where ys' is the result of
an
arbitrary function. folds simply don't work that way, and only give you
access
to the recursive call over the tail, but in a language like Agda, the
termination checker would flag even this definition, and you'd have to,
for
instance, write a proof that this actually does terminate, and do
induction on
the structure of the proof, or use some other such technique for writing
non-
structurally recursive functions.
-- Dan
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Fold that quits early?

Ryan Ingram