The uniqueness of the definition of Nothing only holds up to isomorphism.<br><br>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. <br>
<br>The mathematician on the other hand can put on his fuzzy goggles and just say that they are all the same up to isomorphism. =)<br><br>-Edward Kmett<br><br><div class="gmail_quote">On Tue, Mar 30, 2010 at 3:45 PM, <span dir="ltr"><<a href="mailto:wagnerdm@seas.upenn.edu">wagnerdm@seas.upenn.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">Quoting Ashley Yakeley <<a href="mailto:ashley@semantic.org" target="_blank">ashley@semantic.org</a>>:<br>
<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
data Nothing<div class="im"><br>
<br>
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.<br>
</div></blockquote>
<br>
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<br>
<br>
data Nothing2<br>
<br>
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...)<br>
<br>
~d<div><div></div><div class="h5"><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br>