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 , [EMAIL PROTECTED] 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
