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

[Yitzchak Gale]

I wrote:
>> 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 _|_.

Jonathan Cast wrote:
> 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...
> But by your rule, Left undefined = Right undefined...
> Which is a contradiction...

OK, thanks.

> Unless, of course,
> your require your functions to be strict --- then both f and g above
> become illegal, and repairing them removes the problem.

You don't have to make them illegal - just not part
of your notion of "coproduct". That is an entirely
category-theoretic concept, since Empty is bi-universal,
and a morphism is strict iff the diagram

   f
A ---> B
 \     ^
  v    /
 Empty

commutes.

However, the coproduct you get is the one I suggested,
namely Either !A !B, not the one we usually use.

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