Quoting Ashley Yakeley <ash...@semantic.org>:
data Nothing
I avoid explicit "undefined" in my programs, and also hopefully
non-termination. Then the bottomless interpretation becomes useful,
for instance, to consider Nothing as an initial object of Hask
particularly when using GADTs.
Forgive me if this is stupid--I'm something of a category theory
newbie--but I don't see that Hask necessarily has an initial object in
the bottomless interpretation. Suppose I write
data Nothing2
Then if I understand this correctly, for Nothing to be an initial
object, there would have to be a function f :: Nothing -> Nothing2,
which seems hard without bottom. This is a difference between Hask and
Set, I guess: we can't write down the "empty function". (I suppose
unsafeCoerce might have that type, but surely if you're throwing out
undefined you're throwing out the more frightening things, too...)
~d
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
