[Haskell-cafe] Basic question concerning the category Hask (was: concerning data constructors)

[Jonathan Cast]

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 the  
>> function
>> f (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 pattern  
>>> matching
>>> without introducing such a lifting requires a parallel  
>>> implementation
>
> That'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 single  
>>> level of
>>> lifting, 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 have  
>>> few
>>> enough morphisms to get away with this (at least some times),  
>>> Hask is
>>> not 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 what  
> alternative
> constructions exist if they do not - reflect the nature of the  
> structure
> that 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