Hi Lennart,
On Sat, Jan 24, 2009 at 10:47 PM, Lennart Augustsson
You can dream up any semantics you like about bottom, like it has to be () for the unit type. But it's simply not true. I suggest you do some cursory study of denotational semantics and domain theory.
Umh. It's certainly not Haskell, but as far as I can tell, the semantics Bob likes are perfectly fine domain theory. (_|_, _|_) = _|_ is the *simpler* definition of domain-theoretical product (and inl(_|_) = inr(_|_) = _|_ is the simpler definition of domain-theoretical sum), and the unit of this product (and sum) is indeed the type containing only bottom. Lifting everything, as Haskell does, is extra. I suppose it's unusual that Bob wants to lift sums but not products, but there's nothing theoretically fishy about it that I can see. All the best, - Benja P.S. For anybody wanting to brush up: http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf -- Section 3.2. -B