[Haskell-cafe] Product-Categories

[Lyndon Maydwell]

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
>
>
> > [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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130705/6e902bf9/attachment.htm>