[ANN] extended-categories

extended-categories

Ian Milligan
writes:
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
javascript:> writes: 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
javascript:> writes: 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