[Haskell-cafe] Re: ANN: data-category, restricted categories
ashley at semantic.org
Tue Mar 30 16:35:59 EDT 2010
wagnerdm at 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.
More information about the Haskell-Cafe