[Haskell-cafe] Re: Article review: Category Theory

[apfelmus at quantentunnel.de]

Ulf Norell wrote:
> In the section on the category laws you say that the identity morphism
> should satisfy
> 
>   f . idA = idB . f
> 
> This is not strong enough. You need
> 
>   f . idA = f = idB . f
> 
> Unfortunately, fixing this means that the category Hask is no longer a
> category since
> 
>   _|_ . id = \x -> _|_ =/= _|_

Neil Mitchell wrote:
>> Isn't _|_ = \x -> _|_?
> 
> _|_ `seq` () = _|_
> (\x -> _|_) `seq` () = ()
> 
> Whether this is the fault of seq or not is your call...

Subtle, subtle.

>From the point of view of denotational semantics, the functions (x
\mapsto _|_) and _|_ are the same as equality and the semantic
approximation order are defined point-wise. Usually, the morphisms of
some category arising from a (non-normalizing or polymorphic) lambda
calculus are given by such partial functions.

The key point about lambda calculi is that the "external" morphisms sets
can be "internalized", i.e. represented as objects of the category
themselves. So, the set of morphisms from 'Integer' to 'Integer' can be
represented by the type 'Integer -> Integer'. But, as the example with
`seq` shows, this is not entirely true. Apparently, Haskell represents
function types in a boxed way, i.e. they are lifted by an extra _|_:

   newtype ClosureInt2Int = Closure (Integer -> Integer)#

Thus, Hask is not a category, at least not as defined in the article.
The problem is that (either) morphisms or the morphism composition ('.')
are not internalized correctly in Haskell.

Regards,
apfelmus