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
