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 > > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
