
wagnerdm@seas.upenn.edu wrote:
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".
Right. It's an unfortunate limitation of the Haskell language that one cannot AFAIK write this: f :: Nothing -> Nothing2; f n = case n of { }; However, one can work around it with this function: never :: Nothing -> a never n = seq n undefined; Of course, this workaround uses undefined, but at least "never" has the property that it doesn't return bottom unless it is passed bottom. -- Ashley Yakeley