[Haskell-cafe] Re: Article review: Category Theory
lennart at augustsson.net
Fri Jan 19 08:18:31 EST 2007
And this is why some of us think that adding polymorphic seq to
Haskell was a mistake. :(
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
>> 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
> 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe