[Haskell-cafe] Fold that quits early?

[Ryan Ingram]

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 <wagner.andrew at gmail.com>:
> 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 <wagner.andrew at gmail.com>
> 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 <dan.doel at gmail.com> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>