# Re: [Haskell-cafe] Basic question concerning the category Hask (was: concerning data constructors)

```On 5 Jan 2008, at 6:03 PM, Yitzchak Gale wrote:

```
```Jonathan Cast wrote:
```
```The normal view taken by Haskellers is that the denotations of
So:
(1) Must be monotone
(2) Must be continuous
(Needn't be strict, even though that messes up the resulting
category substantially).
```
```
I wrote:
```
```I'm not convinced that the category is all that "messed up".
```
```
```
```Well, no coproducts (Haskell uses a lifted version of the coproduct
from CPO).
```
```
What goes wrong with finite coproducts? The obvious thing to
do would be to take the disjoint union of the sets representing the
types, identifying the copies of _|_.
```
```
```
This isn't a coproduct. If we have f x = 1 and g y = 2, then there should exist a function h such that h . Left = f and h . Right = g, i.e.,
```
h (Left x)
= f x
= 1

and
h (Right y)
= g y
= 2

But by your rule, Left undefined = Right undefined, so
1
= h (Left undefined)
= h (Right undefined)
= 2

```
Which is a contradiction. Identifying Left _|_ and Right _|_ produces a pointed CPO, but it's not a coproduct. Unless, of course, your require your functions to be strict --- then both f and g above become illegal, and repairing them removes the problem.
```
```
```What is the lifted version you are referring to?
```
```
```
Take the ordinary disjoint union, and then add a new _|_ element, distinct from both existing copies of _|_ (which are still distinct from each other).
```
```
```
```
``` Of course, Haskell makes things even worse by lifting the
product and exponential objects,
```
```
OK, what goes wrong there, and what is the lifting?
```
```
Again, in Haskell, (_|_, _|_) /= _|_.  The difference is in the function

f (x, y) = 1

```
which gives f undefined = undefined but f (undefined, undefined) = 1. Unfortunately, this means that (alpha, beta) has an extra _|_ element < (_|_, _|_), so it's not the categorical product (which would lack such an element for the same reason as above). This is partly an implementation issue --- compiling pattern matching without introducing such a lifting requires a parallel implementation --- and partly a semantic issue --- data introduces a single level of lifting, every time it is used, and every constructor is completely lazy.
```
```
Functions have the same issue --- in the presence of seq, undefined / = const undefined.
```
```
Extensionality is a key part of the definition of all of these constructions. The categorical rules are designed to require, in concrete categories, that the range of the two injections into a coproduct form a partition of the coproduct, the surjective pairing law (fst x, snd x) = x holds, and the eta reduction law (\ x -> f x) = f holds. Haskell flaunts all three; while some categories have few enough morphisms to get away with this (at least some times), Hask is not one of them.
```
jcc

_______________________________________________