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
