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