Thanks a lot for that Adam.
Glad to hear I wasn't too far off the right track :-)
Regards,
- Lyndon
On Thu, Jul 4, 2013 at 5:34 PM, Adam Gundry
Hi,
On 04/07/13 02:19, Lyndon Maydwell wrote:
I'm wracking my brain trying to figure out a simple, reasonably general, implementation for a category instance for pairs of categories.
So far I've looked at [1], which seems great, but doesn't use the built-in category instance, and [2], which I'm just not sure about.
Unless I misunderstand your question, I think [1] is the way to achieve what you want (indeed the blog post mentions defining a Category instance for product categories). It uses the same Category class as in base, but with the PolyKinds extension turned on, which is necessary if you want objects of the category to be anything other than types of kind *, as the post explains. This generalisation should be in the next release of base [3].
It looks like [2] is defining Cartesian categories, which have an internal product, rather than taking the product of categories. If only we could make a category of categories...
Back to your question, consider the following:
{-# LANGUAGE TypeFamilies, TypeOperators, PolyKinds, DataKinds #-}
module ProductCategory where
import Prelude hiding (id, (.))
class Category cat where id :: cat a a (.) :: cat b c -> cat a b -> cat a c
-- We need the projections from pairs:
type family Fst (x :: (a, b)) :: a type instance Fst '(a, b) = a
type family Snd (x :: (a, b)) :: b type instance Snd '(a, b) = b
-- Now a morphism in the product category of `c` and `d` is a pair of -- a morphism in `c` and a morphism in `d`. Since the objects `s` and -- `t` are pairs, we can project out their components:
data Product c d s t = Product (Fst s `c` Fst t) (Snd s `d` Snd t)
With these definitions, your instance below is accepted.
Ideally I'd like to be able to express something like -
instance (Category a, Category b) => Category (Product a b) where id = Product id id Product o1 o2 . Product i1 i2 = Product (o1 . i1) (o2 . i2)
However, it all falls apart when I actually try to define anything. Is this possible? If not, why not?
Does the above help, or were you stuck on something else?
As far as I can tell the issue boils down to not being able to translate "Category i o" to "Product (Fst i) (Fst o) (Snd i) (Snd o)" without breaking the kind expectation of the category instance.
Please help me, I'm having a bad brain day :-)
Hopefully the above will let you get a bit further, although working with type-level pairs isn't always fun. At the moment, GHC doesn't support eta-expansion of pairs [4], so it can't prove that
x ~ (Fst x, Snd x) for all x :: (a, b)
which rapidly becomes annoying when you try to work with constructions like the product category above.
Adam
[1] - http://twanvl.nl/blog/haskell/categories-over-pairs-of-types [2] -
http://hackage.haskell.org/packages/archive/categories/1.0.6/doc/html/Contro...
[3] http://www.haskell.org/pipermail/libraries/2013-May/020127.html [4] http://hackage.haskell.org/trac/ghc/ticket/7259