[Haskell-cafe] Re: Basic question concerning the category Hask
(was: concerning data constructors)
apfelmus at quantentunnel.de
Sun Jan 6 10:39:44 EST 2008
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)
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 (_|_,_|_)
(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._|_ .
More information about the Haskell-Cafe