### Re: Product-Categories

Adam Gundry <adam.gundry <at> strath.ac.uk>

2013-07-04 07:34:21 GMT

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/Control-Category-Cartesian.html#t:Product
[3] http://www.haskell.org/pipermail/libraries/2013-May/020127.html
[4] http://hackage.haskell.org/trac/ghc/ticket/7259