[Haskell-cafe] Re: ANNOUNCE zeno 0.1.0

[wren ng thornton]

On 11/13/10 8:15 AM, Will Sonnex wrote:
> Infinite values (lazy-evaluation in general) also give Zeno a problem,
> since you can no longer use structure as a well-defined ordering for
> induction. A property such as "reverse (reverse xs) === xs" does not
> work for infinite lists, since you can successfully case-analyse
> values from "xs" but case-analysing "reverse (reverse xs)" will give
> an infinite loop. You could say the values are equal in some sense
> (maybe given infinite computation time) but they do not behave in the
> same way.

Generally speaking the solution for handling possibly infinite 
structures is to use coinduction rather than induction. The reason 
"reverse (reverse xs) === xs" doesn't work for (possibly)infinite lists 
is that we can't prove that reverse.reverse makes any progress (since 
reverse of an infinite list is bottom). But there are plenty of other 
things you could still prove for infinite structures, "map f (map g xs) 
=== map (f.g) xs" for example.

-- 
Live well,
~wren