Jonathan Cast
_|_ 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 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.