[Haskell-cafe] Re: ANN: data-category, restricted categories

[wagnerdm at seas.upenn.edu]

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