On 6 Jan 2008, at 5:32 AM, Yitzchak Gale wrote:

(sorry, I hit the send button)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).Now why is that not the category-theoretic coproduct? h . Left = f and h . Right = g both for _|_ and for finite elements of the types. And it looks universal to me.

`Not quite. The only requirement for h _|_ is that it be <= f x for`

`all x and <= g y for all y. If f x = 1 = g y for all x, y, then both`

`h _|_ = _|_ and h _|_ = 1 are arrows of the category. So the`

`universal property still fails.`

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 thefunctionf (x, y) = 1 which gives f undefined = undefined but f (undefined, undefined) = 1.I don't get that one. Given any f and g, we define h x = (f x, g x). Why do we not have fst . h = f and snd . h = g, both in Hask and StrictHask? fst and snd are strict.

`Again, if f and g are both strict, we have a choice for h _|_ ---`

`either h _|_ = _|_ or h _|_ = (_|_, _|_) will work (fst . h = f and`

`snd . h = g), but again these are different morphisms.`

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).The reason you can't adjoin an extra element to (A,B) in, say, Set, is that you would have nowhere to map it under fst and snd. But here that is not a problem, _|_ goes to _|_ under both.This is partly an implementation issue --- compiling patternmatchingwithout introducing such a lifting requires a parallelimplementationThat's interesting. So given a future platform where parallelizing is much cheaper than it is today, we could conceivably have a totally lazy version of Haskell. I wonder what it would be like to program in that environment, what new problems would arise and what new techniques would solve them. Sounds like a nice research topic. Who is working on it?--- and partly a semantic issue --- data introduces a singlelevel oflifting, every time it is used, and every constructor is completely lazy.Unless you use bangs. So both options are available, and that essentially is what defines Haskell as being a non-strict language.

`(!alpha, !beta) isn't a categorical product, either. snd (undefined,`

`1) = undefined with this type.`

Functions have the same issue --- in the presence of seq,undefined /= const undefined.Right. I am becoming increasingly convinced that the seq issue is a red herring.

Care to give an explanation?

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 havefewenough morphisms to get away with this (at least some times),Hask isnot one of them.That interpretation is not something that is essential in the notion of category, only in certain specific examples of categories that you know.

`I understand category theory. I also know that the definitions used`

`are chosen to get Set `right', which means extensionality in that`

`case, and are then extended uniformly across all categories. This`

`has the effect of requiring similar constructions to those in Set in`

`other concrete categories.`

Product and coproduct in any given category -whether they exist, what they are like if they exist, and whatalternativeconstructions exist if they do not - reflect the nature of thestructurethat the category is modeling.

I understand that. I'm not sure you do.

I am interested in understanding the category Hask that represents what Haskell really is like as a programming language.

Good luck.

Not under some semantic mapping that includes non-computable functions, and that forgets some of the interesting structure that comes from laziness (though that is undoubtably also very interesting).

`Bear in mind in your quest, that at the end of it you'll most likely`

`conclude, like everyone else, that good old equational reasoning is`

`sound for the programs you actually right at least 90% of the time`

`(with appropriate induction principles), and complete for at least`

`90% of what you want to right, and go back to using it exclusively`

`for real programming.`

jcc _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe