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