On 12/21/12 2:35 PM, Chris Smith wrote:
It would definitely be nice to be able to work with a partial Category
class, where for example the objects could be constrained to belong to a
class. One could then restrict a Category to a type level representation
of the natural numbers or any other desired set. Kind polymorphism should
make this easy to define, but I still don't have a good feel for whether it
is worth the complexity.
Actually, what you really want is ConstraintKinds. The following works
just fine in GHC 7.6.1:
{-# LANGUAGE KindSignatures
, ConstraintKinds
, PolyKinds
, TypeFamilies
, MultiParamTypeClasses
, FunctionalDependencies
, FlexibleInstances
, FlexibleContexts
#-}
class Category (c :: k -> k -> *) where
-- | The kind of domain objects.
type DomC c x :: Constraint
-- | The kind of codomain objects.
type CodC c x :: Constraint
-- | The identity morphisms.
id :: (ObjC c x) => c x x
-- | Composition of morphisms.
(.) :: (DomC c x, ObjC c y, CodC c z) => c y z -> c x y -> c x z
-- | An alias for objects in the centre of a category.
type ObjC c x = (Category c, DomC c x, CodC c x)
-- | An alias for a pair of objects which could be connected by a
-- @c@-morphism.
type HomC c x y = (Category c, DomC c x, CodC c y)
Notably, we distinguish domain objects from codomain objects in order to
allow morphisms "into" or "out of" the category, which is indeed helpful
in practice.
Whether there's actually any good reason for distinguishing DomC and
CodC, per se, remains to be seen. In Conal Elliott's variation[1] he
moves HomC into the class and gets rid of DomC and CodC. Which allows
constraints that operate jointly on both the domain and codomain,
whereas the above version does not. I haven't run into the need for that
yet, but I could easily imagine it. It does add a bit of complication
though since we can no longer have ObjC be a derived thing; it'd have to
move into the class as well, and we'd have to somehow ensure that it's
coherent with HomC.
The above version uses PolyKinds as well as ConstraintKinds. I haven't
needed this myself, since the constraints act as a sort of kind for the
types I'm interested in, but it'll definitely be useful if you get into
data kinds, or want an instance of functor categories, etc.
[1]
<https://github.com/conal/linear-map-gadt/blob/master/src/Control/ConstraintKinds/Category.hs>
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
