[Haskell-cafe] Fold that quits early?

[Andrew Wagner]

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/bfa045c3/attachment.htm