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

[Jonathan Cast]

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
>>>> Haskell types are CPPOs.
>>>>  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