On 27 Dec 2007, at 8:38 PM, Albert Y. C. Lai wrote:
Achim Schneider wrote:
[n..] == [m..], the first thing I notice is
n == m && n+1 == m+1
, which already expresses all of infinity in one instance and can be
trivially cancelled to
n == m
, which makes the whole darn thing only _|_ if n or m is _|_,
which no
member of [n..] can be as long as n isn't or 1 or + has funny ideas.
I finally begin to understand my love and hate relationship with
formalisms: It involves cuddling with fixed points while protecting
them from evil data and fixed points they don't like as well as
reduction strategies that don't see their full beauty.
There is a formalism that says [n..]==[n..] is true. (Look for co-
induction, observational equivalence, bismulation, ...)
But, of course, any formalism that says [n..]==[n..] = True
interprets (==) as either not a monotone or not a continuous
function. Saying that [n..] = [n..] for some equivalence relation
doesn't say anything about the value of the Haskell expression [n..]
== [n..].
jcc
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
