Jonathan Cast <[EMAIL PROTECTED]> 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
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.
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe