Quoting Ashley Yakeley
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