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

[Yitzchak Gale]

Hi Andrew,

Andrew Bromage wrote:
> I still say it "isn't a set" in the same way that a group "isn't a set".
> Haskell data types have structure that is respected by Haskell
> 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
Hask morphisms? In two ways, I think:

1. They must be computable.
2. They must satisfy certain strictness criteria involving
   undefined and seq.

(1) can be rather boring, since computability is rarely is
an issue in real-life programming problems.

It seems that some people using concepts from categories in
Haskell would prefer to ignore (2) as well. If so, we have been
reduced to viewing Hask as more or less the same as a small
subcategory of Set, with no additional structure that
is of interest.

In this view, there is nothing special about Haskell, except
for the fact that category-theoretic concepts are a bit
easier to express in Haskell than in many other languages.
So perhaps a better name for this category would be
Turing.

I don't think that ignoring (2) is the right approach. I would
like Hask to reflect the non-strict nature of Haskell, which is
one of its most interesting features.

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

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.

For example: I think that "monads" in Haskell should
satisfy the monad laws in Hask, not just after applying
the forgetful functor to Turing. That means that (>>=)
must be strict in its second argument. That would very
likely not break any existing programs, yet almost none
of the existing monads satisfy this, not even IO.

Regards,
Yitz