[Haskell-cafe] Fold that quits early?

[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 <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
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090124/4531be39/attachment.htm