[ANN] extended-categories
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
Ian Milligan <ianmllgn@gmail.com> writes:
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
Hi Ian, You should definitely also take a look at Edward Kmett's hask library: https://github.com/ekmett/hask He has taken the idea of poly-kinded Category and run with it in that library. To compare, he has: class Category' (p :: i -> i -> *) where type Ob p :: i -> Constraint id :: Ob p a => p a a observe :: p a b -> Dict (Ob p a, Ob p b) (.) :: p b c -> p a b -> p a c John
Hi John, amazingly I hadn't ran into this package. It seems that we take very different approaches to functors. I borrowed the 'data-category' approach of named functors, while hask uses the standard approach of implicit functors. Without explicit functors, there are many functors that we cannot express, such as the product functor or the diagonal functor. I will have to look at hask in more depth, however, I am sure there are many ideas I could borrow. Ian On Tuesday, August 19, 2014 2:40:21 AM UTC-7, John Wiegley wrote:
Ian Milligan <ianm...@gmail.com <javascript:>> writes:
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
Hi Ian,
You should definitely also take a look at Edward Kmett's hask library:
https://github.com/ekmett/hask
He has taken the idea of poly-kinded Category and run with it in that library. To compare, he has:
class Category' (p :: i -> i -> *) where type Ob p :: i -> Constraint id :: Ob p a => p a a observe :: p a b -> Dict (Ob p a, Ob p b) (.) :: p b c -> p a b -> p a c
John _______________________________________________ Haskell-Cafe mailing list Haskel...@haskell.org <javascript:> http://www.haskell.org/mailman/listinfo/haskell-cafe
I've now borrowed the approach of hask: an installation of an arrow is proof that its domain and codomain are objects. This is a great simplification. On Tuesday, August 19, 2014 2:40:21 AM UTC-7, John Wiegley wrote:
Ian Milligan <ianm...@gmail.com <javascript:>> writes:
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
Hi Ian,
You should definitely also take a look at Edward Kmett's hask library:
https://github.com/ekmett/hask
He has taken the idea of poly-kinded Category and run with it in that library. To compare, he has:
class Category' (p :: i -> i -> *) where type Ob p :: i -> Constraint id :: Ob p a => p a a observe :: p a b -> Dict (Ob p a, Ob p b) (.) :: p b c -> p a b -> p a c
John _______________________________________________ Haskell-Cafe mailing list Haskel...@haskell.org <javascript:> http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (2)
-
Ian Milligan -
John Wiegley