[Haskell-cafe] Categories (cont.)

[wren ng thornton]

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 at -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