[Haskell-cafe] Re: Wikipedia on first-class object

[Jonathan Cast]

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