extended-categories <github.com/ian-mi/extended-categories> is an implementation of categories designed to make use of GHC's recently enriched kind system. This project is a work in progress (only a few basic constructs are implemented), but your comments are welcomed. extended-categories requires a recent version of GHC (I have only tested it with 7.8.3).

Categories are poly-kinded and have an Object constraint family:

class Category m where
    type Object (m :: k -> k -> *) (a :: k) :: Constraint
    id :: Object m a => m a a
    (.) :: (Object m a, Object m b, Object m c) => m b c -> m a b -> m a c

This means in addition to our usual categories of kind * -> * -> * we can define categories of other kinds, for example (:-) from the constraints package forms a category with kind Constraint -> Constraint -> * (whose instance is used in this package)!

Functors are named (tagged) as done in the data-category package. This allows a much wider variety of functors to be defined. Additionally functors must provide proof that they are closed under the object constraint, i.e. forall a. Object (Domain f c1) a :- Object (Codomain f c2) (FMap f a).

For any two categories c1: k1 -> k1 -> * and c2: k2 -> k2 -> *, the product category (c1 :><: c2) has kind (k1, k2) -> (k1, k2) -> *. The functor (Diag c) is defined to be the functor from c to c :><: c which sends the object X to '(X, X) and morphism f to the morphism f :><: f. Categories which contain their products (the class ProductCategory) are defined by the universal property described here <http://en.wikipedia.org/wiki/Universal_morphism#Products>, i.e. by a terminal morphism, for every object a and b of c, from (Diag c) to the object '(a, b) of c :><: c. From this terminal morphism, the functions fst, snd, (&&&), and (***), as well as the product functor from c :><: c to c mapping '(a, b) to a >< b and f :><: g to f *** g, are defined.

Here are some examples of how this works with the standard Haskell functors:

*Functor> fmap (CanonicalF :.: CanonicalF) P.succ [P.Just 2, P.Nothing]
[Just 3,Nothing]

*Product> fmap (CanonicalF :.: ProductF) ((P.+1) :><: (P.+2)) [(1,2), (3,4), (5,6)]
[(2,4),(4,6),(6,8)]

or alternatively fmap CanonicalF ((P.+1) *** (P.+2)) [(1,2), (3,4), (5,6)]

Next I will likely be adding more instances as well as some documentation.

Thanks for reading,
Ian Milligan