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

wagnerdm at seas.upenn.edu wagnerdm at seas.upenn.edu
Tue Mar 30 15:45:46 EDT 2010

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...)


More information about the Haskell-Cafe mailing list