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

Jonathan Cast jonathanccast at fastmail.fm
Sun Jan 6 00:38:19 EST 2008

```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

```