[Haskell-cafe] Re: Basic question concerning the category Hask (was: concerning data constructors)
Yitzchak Gale wrote: I wrote: ...it was recently claimed on this list that tuples are not products in that category. I've not been convinced yet. I'm going to try convince you :) The crucial problem of Haskell's product is that (_|_,_|_) ≠ _|_ but that the two projections fst :: (A,B) - A snd :: (A,B) - B cannot distinguish between both values. But if (,) were a categorial product, fst and snd would completely determine it. We would have the universal property that for every f :: C - A g :: C - B there is a _unique_ morphism f g :: C - (A,B) subject to f = fst . (f g) g = snd . (f g) In other words, there is a unique function () :: forall c . (c - A) - (c - B) - (c - (A,B)) f g = \c - (f c, g c) In the particular case of C=(A,B), f=fst and g=snd , the identity function is such a morphism which means fst snd = id due to uniqueness. But id _|_ ≠ id (_|_,_|_) while clearly (fst snd) _|_ = (fst snd) (_|_,_|_) Derek Elkins wrote: 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. Note that the problem with (.) is seq's fault (pun intended :) Otherwise, it would be impossible to distinguish _|_ from its eta-expansion \x._|_ . Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Basic question concerning the category Hask (was: concerning data constructors)
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. Dominic. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Basic question concerning the category Hask (was: concerning data constructors)
On 6 Jan 2008, at 12:27 PM, Dominic Steinitz wrote: 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; Right. But category theory is nevertheless `backward compatible' with set theory, in the sense that the category theoretic constructions in a category satisfying ZFC will be the same constructions we are familiar with already. The category-theoretic definitions, when specialized to Set, are precise (up to natural isomorphism) definitions of the pre-existing concepts of cartesian products, functions, etc. in Set. Or, to put it another way, the category-theoretic definitions are generalizations of those pre- existing concepts to other categories. Hask has a structure that is Set-like enough that these concepts generalize very little when moving to Hask. 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? By `extensionality' I mean the equalities which follow from using standard set-theoretic definitions for functions, products, coproducts, etc. --- surjective pairing, eta-contraction, etc. My understanding is that, in fact, the category-theoretic definitions are designed to capture those equations in diagrams that can be used as definitions in arbitrary categories. It's possible to view those definitions, then, as more fundamental descriptions of the concepts than what they generalize, but the fact that they are generalizations of the ideas from Set shows up in categories similar to Set (and Hask is certainly more similar to Set than, say, Vec). jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
