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 <ekm...@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, <wagne...@seas.upenn.edu> wrote:
Quoting Ashley Yakeley <ash...@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
