[Haskell-cafe] Fold that quits early?
wagner.andrew at gmail.com
Sat Jan 24 18:07:06 EST 2009
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
>> > of folds that potentially "quit" early. but not sure where I saw that,
>> > 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
>> 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
>> recursion. The problem is in your inductive case, where you don't just
>> 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
>> 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,
>> 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
>> structurally recursive functions.
>> -- Dan
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe