[Haskell-cafe] Fold that quits early?
Dan Doel
dan.doel at gmail.com
Sat Jan 24 12:11:14 EST 2009
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
More information about the Haskell-Cafe
mailing list