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@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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe