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

[Lennart Augustsson]

And this is why some of us think that adding polymorphic seq to  
Haskell was a mistake. :(

	-- Lennart


On Jan 19, 2007, at 08:05 , apfelmus at quantentunnel.de wrote:

> 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe