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