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
