[Haskell-cafe] Fold that quits early?
Ryan Ingram
ryani.spam at gmail.com
Sat Jan 24 22:16:20 EST 2009
foldr f z xs =
x0 `f` (x1 `f` (x2 `f` ... (xN `f` z) ...))
In particular, note that if f is a total function, xs is finite and
totally defined, and z is totally defined, then the result of this
fold is totally defined.
Now consider your "f" (rewritten slightly)
f x xs
| null xs = []
| p x = []
| otherwise = foldr f (x:xs) (g x xs)
with these definitions:
c _ = False
g = (:)
c and g are definitely total functions, so what happens when we
evaluate f 0 [1]?
f 0 [1]
= foldr f [0,1] [0,1]
= let t1 = foldr f [0,1] [1] in f 0 $ t1
= let t1 = foldr f [0,1] [1] in foldr f (0 : t1) (0 : t1)
= let t1 = foldr f [0,1] [1]
t2 = foldr f (0:t1) t1
in f 0 t2
etc.; this is clearly non-terminating.
Therefore there is no way to make f into a fold.
Any errors in my logic?
-- ryan
2009/1/24 Andrew Wagner <wagner.andrew at gmail.com>:
> Ahem. That's what happens when you don't type-check your brainstorming
> before barfing it out, kids. Sorry about that. Let's try this again:
>
> f _ [] = []
> f y x | c y = []
> | otherwise = foldr f (y:x) (g y x)
>
> I've got a fold on the inside now, but I'm pretty sure the whole thing is
> just a fold. Not quite there yet, though...
>
> On Sat, Jan 24, 2009 at 1:42 PM, Andrew Wagner <wagner.andrew at gmail.com>
> wrote:
>>
>> 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
>>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
More information about the Haskell-Cafe
mailing list