
On 25 Jan 2009, at 00:01, Benja Fallenstein wrote:
Hi Lennart,
On Sat, Jan 24, 2009 at 10:47 PM, Lennart Augustsson
wrote: 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.
Yep, this is part of the insight that Conal helped me have – I sense tomorrow is gonna be spent with much blog writing. Bob