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

[Conor McBride]

Getting back to the question, whatever happened to empty case  
expressions? We should not need bottom to write total functions from  
empty types.

Correspondingly, we should have that the map from an empty type to  
another given type is unique extensionally, although it may have many  
implementations. Wouldn't that make any empty type initial? Of course,  
one does need one's isogoggles on to see the uniqueness of the initial  
object.

An empty type is remarkably useful, e.g. as the type of free variables  
in closed terms, or as the value component of the monadic type of a  
server process. If we need bottom to achieve vacuous satisfaction,  
something is a touch amiss.

Cheers

Conor

On 30 Mar 2010, at 22:02, Edward Kmett <ekmett at gmail.com> wrote:

> 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100330/051be974/attachment.html