[Haskell-cafe] ANN: data-category, restricted categories

[Sjoerd Visscher]

Hi everybody,

At ZuriHac I released data-category. It is an implementation of several category-theoretical constructions.

I started this library to learn about both category theory and type level programming, so I wanted to implement the CT concepts as directly as possible. This in contrast to the excellent category-extras library, which (I think) also tries to be as useful as possible.

CT is about studying categories, so for data-category I wanted to implement all kinds of categories. The Control.Category module unfortunately requires you to implement id :: cat a a (for all a), which means it only supports categories that have exactly the same objects as Hask. So Data.Category contains an implementation of restricted categories, using inspiration from Oleg's restricted monads.

It is well known that the Functor class also is a bit limited, as it only supports endofunctors in Hask. But there's another problem, if you want to define the identity functor, or the composition of 2 functors, then you have to use newtype wrappers, which can get in the way. Data.Category has an implementation of functors which solves this by using type families. Functors are represented by labels, and the type family F turns the label into the actual functor. F.e. type instance F List a = [a], type instance F Id a = a.

The current version contains:
- categories
  - Void, Unit, Pair (discrete categories with 0, 1 and 2 objects respectively)
  - Boolean
  - Omega, the natural numbers as an ordered set (ω)
  - Monoid
  - Functor, the category of functors from one category to another
  - Hask
  - Kleisli
  - Alg, the category of F-Algebras
- functors
  - the identity functor
  - functor composition
  - the constant functor
  - the co- and contravariant Hom-functors
  - the diagonal functor
- natural transformations
- universal arrows
- limits and colimits (as universal arrows from/to the diagonal functor)
  - using Void as index category this gives initial and terminal objects
    - f.e. in Alg the arrows from the initial object are catamorphisms
  - using Pair as index category this gives products and coproducts
    - f.e. in Omega they are the minimum and maximum and in Boolean and and or.
- adjunctions

Of course the are still a lot of things missing, especially in the details. And I'm a category theory beginner, so there will probably be some mistakes in there as well. F.e. Edward Kmett doesn't like () being the terminal object in Hask, which I thought I understood, but after thinking about it a bit more I don't.

You can find data-category on hackage and on github:
http://hackage.haskell.org/package/data-category
http://github.com/sjoerdvisscher/data-category

greetings,
Sjoerd Visscher