[Haskell-cafe] Monad laws in presence of bottoms
wren ng thornton
wren at freegeek.org
Wed Feb 22 07:40:27 CET 2012
On 2/21/12 11:54 AM, Dan Doel wrote:
> On Tue, Feb 21, 2012 at 10:44 AM, wren ng thornton<wren at freegeek.org> wrote:
>> That's a similar sort of issue, just about whether undefined ==
>> (undefined,undefined) or not. If the equality holds then tuples would be
>> domain products[1], but domain products do not form domains!
>> ...
>> [1] Also a category-theoretic product.
>
> This doesn't make much sense to me, either. If it's a category
> theoretic product in a category of domains, then the product must be a
> domain, no?
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 category-theoretic product of A and B is just some triple (C, pi_A :
C -> A, pi_B : C -> B) such that forall D, forall f : D -> A, and forall
g : D -> B, there exists a unique h : D -> C such that f = pi_A . h and
g = pi_B . h ---in other words, it's the limit of a functor from the
category with two objects and no morphisms which maps one object to A
and the other object to B.
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.
However, the domain product is not a category-theoretic product in
pDCPO. First off, the objects in pDCPO are domains, but since the domain
product of A and B has no bottom it can't be a domain, so it can't be an
object in pDCPO. Moreover, the morphisms in pDCPO will preserve the
domain structure--- but there's no way to do that for a map from some
domain C to the domain product of A and B, because there's no way to map
the bottom of C to the bottom of the domain product (because there isn't
one!).
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).
For more on the category-theoretic study of domain theory, see
<http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf>. You can search
the pdf for "pointed dcpo" to jump to the relevant sections. Of course
there are many different category-theoretic formalizations of domain
theory, pDCPO is just one of them. To get a survey of the terrain, you
may want to take a look at
<http://seclab.web.cs.illinois.edu/wp-content/uploads/2011/04/Gunter85.pdf>.
For a more direct introduction to domain theory and its application to
lazy languages, see Geoffrey Burn's _Lazy Functional Languages: Abstract
Interpretation and Compilation_.
--
Live well,
~wren
More information about the Haskell-Cafe
mailing list