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