[Haskell-cafe] Basic question concerning the category Hask (was:
concerning data constructors)
jonathanccast at fastmail.fm
Sun Jan 6 00:38:19 EST 2008
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.
>>>> (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,
h (Left x)
= f x
h (Right y)
= g y
But by your rule, Left undefined = Right undefined, so
= h (Left undefined)
= h (Right undefined)
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
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.
More information about the Haskell-Cafe