Lyndon Maydwell | 4 Jul 03:19 2013
Picon

Product-Categories

Hi Café.

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.

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?

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 :-)


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Adam Gundry | 4 Jul 09:34 2013
Picon
Picon

Re: Product-Categories

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
Lyndon Maydwell | 5 Jul 02:04 2013
Picon

Re: Product-Categories

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 <adam.gundry <at> strath.ac.uk> wrote:
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
[3] http://www.haskell.org/pipermail/libraries/2013-May/020127.html
[4] http://hackage.haskell.org/trac/ghc/ticket/7259


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane