[Haskell-cafe] Re: Basic question concerning the category Hask
(was: concerning data constructors)
dominic.steinitz at blueyonder.co.uk
Sun Jan 6 15:27:04 EST 2008
Jonathan Cast <jonathanccast <at> fastmail.fm> writes:
> >>> 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.
Referring to my copy of "Sheaves in Geometry and Logic", Moerdijk and Mac Lane
state that "in 1963 Lawvere embarked on the daring project of a purely
categorical foundation of all mathematics". Did he fail? I'm probably
misunderstanding what you are saying here but I didn't think you needed sets to
define categories; in fact Set is a topos which has far more structure than a
category. Can you be clearer what you mean by extensionality in this context?
And how it relates to Set?
On a broader note, I'm pleased that this discussion is taking place and I wish
someone would actually write a wiki page on why Haskell isn't a nicely behaved
category and what problems this causes / doesn't cause. I wish I had time.
More information about the Haskell-Cafe