[Haskell-cafe] Fold that quits early?

[Dan Doel]

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