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

On 27 Dec 2007, at 4:54 PM, Achim Schneider wrote:

Jonathan Cast wrote:

...

_|_ is the denotation of every Haskell expression whose denotation is _|_.

Mu.

...

Why take away _|_?

Because, when zenning about

instance (Eq a) => Eq [a] where [] == [] = True (x:xs) == (y:ys) = x == y && xs == ys _xs == _ys = False

and

[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

Danger, Will Robinson! Cancellation derives from valid equations, it does not lead to them. (x^2 - 1)/(x - 1) /= 2 when x = 1, however many times you cancel it.

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.

Love formalisms or hate them as much as you want. They still define Haskell's semantics. jcc