[Haskell-cafe] Constrained Category, Arrow, ArrowChoice, etc?

[Sjoerd Visscher]

Hi Conal,

I have a package data-category that should be able to do this. 
http://hackage.haskell.org/package/data-category

I tried implementing your linear map, and this is the result:
https://gist.github.com/sjoerdvisscher/5547235

I had to make some changes to your linear map data type, because it wasn't a valid category (which of course depends on how you define what it means for a data type to be a category). There were 2 problems:

1. data-category has a minimal requirement for data types to be a category: every value in the data type has to be a valid arrow. The fact that you needed to add constraints at the arrow level shows that this is not the case for (:-*). The problem is that Dot is under-constrained. Apparently it is not enough for b to be an inner space. What you need is VS2 b (Scalar b). I think this requirement makes sense: if a value is not a valid arrow, it should not be possible to create it in the first place!

2. (:-*) is not really one category, it is a family of categories: one for each scalar field. This isn't really a problem for the Category class, because a disjoint union of categories is also a category, but it is a problem for products. Because for products you're required to be able to take the product of any 2 objects. But in the case of (:-*), you can only take the product of objects with the same scalar field. So I changed a :-* b to LM s a b, with Scalar a ~ Scalar b ~ s.

I should probably explain a bit about data-category. The problem with the Category class from base is id, with type forall a. cat a a. This assumes that every Haskell type is an object in the category. So one possibility is to add a constraint: forall a. IsObj cat a => cat a a. While you certainly can get quite far with this, at some point it start to get very hard to convince that all constraints are satisfied. 

Through trial and error I found out that what works best is to have a proof value for each object, and there's one value readily available: the identity arrow for that object. But this then turns id into cat a a -> cat a a, which is quite useless. So I had to borrow from the arrows-only description of categories, which has source and target operations that give the source and target identity arrows for each arrow.

Because of the requirement that every value is a valid arrow, there's no need to change the definition of composition.

In the code you can see that I have to do a lot of pattern matching. This is to make the constraints inside the arrows available.

Admittedly passing around proof values instead of relying on constraints gives the whole library quite a unhaskelly feel, but it's the only way I could find that really works well. And often it is possible to provide a public API for a specific category that constructs the proof values from the constraints, like I have done with fstL and sndL in the gist.

I hope this helps you implement your ideas further. Your reimagining matrices post was really superb and I'd love to learn more!

greetings,
Sjoerd

On May 8, 2013, at 12:09 AM, Conal Elliott <conal at conal.net> wrote:

> I'm using a collection of classes similar to Category, Arrow, ArrowChoice, etc (though without arr and with methods like fst, snd, dup, etc). I think I need some associated constraints (via ConstraintKinds), so I've tried adding them. However, I'm getting terribly complex multiplication of these constraints in the signatures of method defaults and utility functions, and I don't know how to tame them. Has anyone tried adding associated constraints to Category etc?
> 
> Thanks, -- Conal
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130509/e8dbc688/attachment.htm>