Actually, I think I can rewrite it this way:<br><br>f xs [] = False<br>f xs (y:ys) | any c ys' = True<br> | otherwise = f (f (y:xs) ys') ys<br> where ys' = g y ys<br><br><div class="gmail_quote">
This should help, I think.<br><br>On Sat, Jan 24, 2009 at 12:11 PM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div><div></div><div class="Wj3C7c">On Saturday 24 January 2009 11:39:13 am Andrew Wagner wrote:<br>
> This is almost a fold, but seemingly not quite? I know I've seem some talk<br>
> of folds that potentially "quit" early. but not sure where I saw that, or<br>
> if it fits.<br>
><br>
> f xs [] = False<br>
> f xs (y:ys) | any c ys' = True<br>
><br>
> | otherwise = f (nub (y:xs)) (ys' ++ ys)<br>
><br>
> where ys' = g y xs<br>
<br>
</div></div>Quitting early isn't the problem. For instance, any is defined in terms of<br>
foldr, and it works fine on infinite lists, quitting as soon as it finds a<br>
True. As long as you don't use the result of the recursive call (which is the<br>
second argument in the function you pass to foldr), it will exit early.<br>
<br>
The problem is that your function doesn't look structurally recursive, and<br>
that's what folds (the usual ones, anyway) are: a combinator for structural<br>
recursion. The problem is in your inductive case, where you don't just recurse<br>
on "ys", you instead recurse on "ys' ++ ys", where ys' is the result of an<br>
arbitrary function. folds simply don't work that way, and only give you access<br>
to the recursive call over the tail, but in a language like Agda, the<br>
termination checker would flag even this definition, and you'd have to, for<br>
instance, write a proof that this actually does terminate, and do induction on<br>
the structure of the proof, or use some other such technique for writing non-<br>
structurally recursive functions.<br>
<font color="#888888"><br>
-- Dan<br>
</font></blockquote></div><br>