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

wagnerdm at seas.upenn.edu wagnerdm at seas.upenn.edu
Tue Mar 30 18:47:27 EDT 2010

I believe I was claiming that, in the absence of undefined, Nothing  
and Nothing2 *aren't* isomorphic (in the CT sense).

But this is straying dangerously far from Ashley's point, which I  
think is a perfectly good one: Hask without bottom is friendlier than  
Hask with bottom.


Quoting Edward Kmett <ekmett at gmail.com>:

> The uniqueness of the definition of Nothing only holds up to isomorphism.
> This holds for many unique types, products, sums, etc. are all subject to
> this multiplicity of definition when looked at through the concrete-minded
> eye of the computer scientist.
> The mathematician on the other hand can put on his fuzzy goggles and just
> say that they are all the same up to isomorphism. =)
> -Edward Kmett
> On Tue, Mar 30, 2010 at 3:45 PM, <wagnerdm at seas.upenn.edu> wrote:
>> 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
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe

More information about the Haskell-Cafe mailing list