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

[Ashley Yakeley]

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.

-- 
Ashley Yakeley