[Haskell-cafe] Fold that quits early?

[Ryan Ingram]

My point is that without further knowledge of this function, it's not
possible to simplify into a fold.  For f to be a fold, the result
would have to terminate for *every* total function g; given that there
are some total functions for which f does not terminate, f cannot be a
fold.

It's possible that the particular combination of f and g that you have
in mind *does* simplify to a fold, but the current function cannot,
unless I've made a mistake.

  -- ryan

On Sat, Jan 24, 2009 at 7:26 PM, Andrew Wagner <wagner.andrew at gmail.com> wrote:
> There's at least one thing; I won't call it a flaw in your logic, but it's
> not true of my usage. Your definition always produces a non-null list. The
> particular g in my mind will eventually produce a null list, somewhere down
> the line. I think if that's true, we can guarantee termination.
>
> On Sat, Jan 24, 2009 at 10:16 PM, Ryan Ingram <ryani.spam at gmail.com> wrote:
>>
>> 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
>> >
>> >
>
>