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

[wagnerdm at seas.upenn.edu]

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.

~d

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