[Haskell-cafe] Monad laws in presence of bottoms

[Dan Doel]

On Wed, Feb 22, 2012 at 1:40 AM, wren ng thornton <wren at freegeek.org> wrote:
> It's a category-theoretic product, but not for the category of domains. Let
> Set be the category of sets and set-theoretic functions. And let pDCPO be
> the category of (pointed) domains and their homomorphisms.
>
> The (domain-theoretic) domain product was discussed in my previous message
> to MigMit. It's a category-theoretic product in Set (among other categories)
> because the necessary morphisms exist and they satisfy the necessary
> equations. Moreover, in Set the domain product coincides with the cartesian
> product (we just forget about the orderings on the input domains and the
> resulting product). Hence, since the cartesian product is a
> category-theoretic product for Set, we know that the domain product must be
> a category-theoretic product in Set.

Well, like Miguel, I don't see the problem with choosing the ordering:

    (a,b) <= (a', b') iff a <= a' and b <= b'

This makes (a0, b0) the bottom element. The only difference with
Haskell's tuple types is that it lacks an extra element below (a0,
b0); it's unlifted.

It also seems to me that this _is_ the correct product for domains,
unless I'm still sketchy on what you mean by domain. I don't think it
matters that we're only considering strict homomorphisms.

> Conversely, the smash product is a category-theoretic product in pDCPO, but
> not in Set. Since every domain homomorphism must map bottoms to bottoms, it
> follows that f(d0) = a0 and g(d0) = b0. From this we have the necessary
> continuity to ensure that C, pi_A, and pi_B all exist in pDCPO. However,
> since there exist set-theoretic functions f and g which do not have that
> special property, the smash product is going to lose information about the
> non-bottom component of the product and so it cannot satisfy the necessary
> category-theoretic equations (in Set).

The smash product is not a product for domains (in general), either.
You are not allowed to throw away the components for such a product,
because given a homomorphism f that maps everything to a0, pi_B .
<f,g> maps everything to b0, regardless of what g is.

-- Dan