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