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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
