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

[apfelmus]

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