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

```I wrote:
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 _|_.

Jonathan Cast wrote:
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...
But by your rule, Left undefined = Right undefined...

OK, thanks.

Unless, of course,
your require your functions to be strict --- then both f and g above
become illegal, and repairing them removes the problem.

You don't have to make them illegal - just not part
of your notion of coproduct. That is an entirely
category-theoretic concept, since Empty is bi-universal,
and a morphism is strict iff the diagram

f
A --- B
\ ^
v/
Empty

commutes.

However, the coproduct you get is the one I suggested,
namely Either !A !B, not the one we usually use.

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

___

```

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

```On Wed, 2008-01-02 at 15:49 +0200, Yitzchak Gale wrote:

[...]

Some people are worried that this version of Hask is missing
certain nice properties that one would like to have. For
example, it was recently claimed on this list that tuples
are not products in that category. (Or some such. I would be
interested to see a demonstration of that.)

Johnathan has given such a demonstration (and it has been demonstrated
many times on this list since it's creation, it's well-known).

I am not impressed by those complaints. As usual in category
theory, you define corresponding notions in Hask, and prove
that they are preserved under the appropriate functors.
That should always be easy. And if ever it is not, then you
have discovered an interesting non-trivial consequence of
laziness that deserves study.

You are right not to be impressed by such complaints, but you
misrepresent people's views on this by saying that the worry about
such problems.

As you say (people say), these properties [that Hask is cartesian closed
to start] would be nice to have and are very convenient to assume which
is often safe enough.  Certainly computer scientists of a categorical
bent have developed (weaker) notions to use; namely, monoidal,
pre-monoidal, Freyd, and/or kappa categories and no doubt others.  Using
these, however, removes some of the allure of using a categorical
approach.  Also, there is a Haskell-specific problem at the very get-go.
The most obvious choice for the categorical composition operator
assuming the obvious choice for the arrows and objects does not work,
it does not satisfy the laws of a category assuming the = used in them
is observational equality.  Namely, id . f /= f /= f . id for all
functions f, in particular, it fails when f = undefined.  This can
easily be fixed by making the categorical (.) strict in both arguments
and there is no formal problem with it being different from Haskell's
(.), but it certainly is not intuitively appealing.

___

```

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

```(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.

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.

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.

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.

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. 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 am interested in understanding the category Hask that represents
what Haskell really is like as a programming language. 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).

-Yitz
___

```

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

```I wrote:
...it was recently claimed on this list that tuples
are not products in that category.

Derek Elkins wrote:
Johnathan has given such a demonstration (and it has been demonstrated
many times on this list since it's creation, it's well-known).

We're still working on it. I've not been convinced yet.

Perhaps this should be on a nice wiki page somewhere.
I tried to convince David House to put it in the Wikibook
chapter, but he is right, that needs to simpler. There is
some discussion on the talk page for that
chapter, but no one spells out the details there, either.

You are right not to be impressed by such complaints, but you
misrepresent people's views on this by saying that they worry about
such problems.

Sorry, I hope I am not misrepresenting anyone. I just
notice that people make assumptions about a so-called
category Hask, derive various conclusions, then mention
that they are not really true. Perhaps it is only me who is
worried.

As you say (people say), these properties [that Hask is cartesian closed
to start] would be nice to have and are very convenient to assume which
is often safe enough.

I'd like to understand better what is true, so that I can understand
what is safe.

Certainly computer scientists of a categorical
bent have developed (weaker) notions to use; namely, monoidal,
pre-monoidal, Freyd, and/or kappa categories and no doubt others.  Using
these, however, removes some of the allure of using a categorical
approach.

It would be nice to distill out of that the basics that are needed
to get the properties that we need for day-to-day work in

Also, there is a Haskell-specific problem at the very get-go.
The most obvious choice for the categorical composition operator
assuming the obvious choice for the arrows and objects does not work...
...This can
easily be fixed by making the categorical (.) strict in both arguments
and there is no formal problem with it being different from Haskell's
(.), but it certainly is not intuitively appealing.

I'm not sure it's so bad. First of all, not only is it not a formal
problem, it's also not really a practical problem - there will rarely
if ever be any difference between the two when applied in real
programs.

My opinion is that there would not be any problem with using
that version as (.) in the Prelude. Even if we never do, at least
we should then use (.!) when we state the so-called Monad laws.
That is bound to cause problems.

And it would be so easy to fix in most cases - just require monad
bind to be strict on the second parameter.

Thanks,
Yitz
___

```

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

```
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.

Yeah, but there could be more functions from Either X Y to Z than
pairs of functions from X to Z and from Y to Z.

For example, if z :: Z, then you have two functions h1 and h2 such
that h1 . Left = const z and h1 . Right = const z and the same holds
for h2. Namely,

h1 = const z

h2 = either (const z) (const z)

This functions are different : h1 (_|_) = z while h2 (_|_) = (_|_).
And if Either X Y was a category-theoretic coproduct, then the
function from Either X Y to Z would be UNIQUELY determined by it's
restrictions to X and Y.

___

```

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

```
On 6 Jan 2008, at 3:55 AM, Yitzchak Gale wrote:

I wrote:

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 _|_.

Jonathan Cast wrote:

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...
But by your rule, Left undefined = Right undefined...

OK, thanks.

Unless, of course,
your require your functions to be strict --- then both f and g above
become illegal, and repairing them removes the problem.

You don't have to make them illegal - just not part

We're talking past each other --- what is the distinction you are
making?

jcc

___

```

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

```
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),

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

___

```

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

```Jonathan Cast wrote:
The normal view taken by Haskellers is that the denotations of
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 _|_.

What is the lifted version you are referring to?

Of course, Haskell makes things even worse by lifting the
product and exponential objects,

OK, what goes wrong there, and what is the lifting?

Thanks,
Yitz
___

```

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

```
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
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

___

```

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

```Hi Jonathan,

I wrote:
So in what way are Set morphisms restricted from being

Jonathan Cast wrote:
The normal view taken by Haskellers is that the denotations of

CPPO?

So:

(1) Must be monotone
(2) Must be continuous

Could you please define what you mean by those terms
in this context?

(Needn't be strict, even though that messes up the resulting category
substantially).

I'm not convinced that the category is all that messed up.

Thanks,
Yitz
___

```

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

```Jonathan Cast wrote:
The normal view taken by Haskellers is that the denotations of

I wrote:
CPPO?

(1) Must be monotone
(2) Must be continuous

Could you please define what you mean by those terms
in this context?

Jens Blanck wrote:
The extra P would stand for pointed (has a least element, bottom), this is
common in some communities. To me though, a cpo (complete partial order) is
closed under directed suprema and the empty set is directed so bottom is
already required. The category of cpos in not cartesian closed. For
denotational semantics I believe the subcategory of Scott domains are what
is usually considered.

Continuous functions on cpos are by definition monotone and they respect
directed suprema.

Thanks!
Yitz
___

```

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

```
On 3 Jan 2008, at 3:40 AM, Jens Blanck wrote:

The normal view taken by Haskellers is that the denotations of

CPPO?

So:

(1) Must be monotone
(2) Must be continuous

Could you please define what you mean by those terms
in this context?

(Needn't be strict, even though that messes up the resulting
category

substantially).

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).  Of course, Haskell makes things even worse by lifting the
product and exponential objects, as well, which come to think of it
is unnecessary even in the category of CPPOs and not necessarily
strict continuous functions.

The extra P would stand for pointed (has a least element, bottom),
this is common in some communities. To me though, a cpo (complete
partial order) is closed under directed suprema and the empty set is
directed so bottom is already required.

Not so.  A set is directed iff every finite subset has an upper bound
in the set; {} is finite, so it must have an upper bound in the set.
So directed sets must be non-empty.  (So CPOs needn't be pointed).

jcc

___

```

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

```
On 2 Jan 2008, at 5:49 AM, Yitzchak Gale wrote:

Hi Andrew,

Andrew Bromage wrote:
I still say it isn't a set in the same way that a group isn't a
set.

homomorphisms.  Sets don't.

Ah, that's certainly true. But what is that additional structure?

In categories that have a forgetful functor to Set, the interesting
part of their structure comes from the fact that their
morphisms are only a proper subset of the morphisms
in Set.

So in what way are Set morphisms restricted from being

The normal view taken by Haskellers is that the denotations of

(1) Must be monotone
(2) Must be continuous

(Needn't be strict, even though that messes up the resulting category
substantially).

jcc

___