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

Hi Sjoerd, Thanks very much for the help sorting out options for more flexibility in Category instances. I like how you spotted and removed the id problem. I’ve cloned your gist https://gist.github.com/conal/5549861 and tried out an idea to simplify verifying the required constraints on linear map values. About the change from a ⊸ b to LM s a b, I originally used the latter style (as a scalar-parametrized family of categories, using the explicit sparameter to VS, VS2, etc), but I greatly prefer the former notation, especially when type-set. I guess with lhs2tex, we could typeset “LM s a b” by placing the “s” under the (multi)linear map symbol or some such, or perhaps even omit it. Am I right in thinking that the first two (Obj) arguments proj1 and proj2serve as proofs that the types involved are legitimate for the category ( k)? 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 wonder whether this trick is compatible for my goals with circuit synthesis and analysis. I want to express fairly general computations over Category etc and then type-instantiate them into multiple interpretations in the form of categories of functions (for CPU execution), circuits, strictness/demand analysis, timing analysis, and hopefully others. (Rather than requiring the code to be written in this obscure categorical form, I intend to transform conventional pointful (function-specific) code via a (to-be-written) GHC plugin. Our goal is accept arbitrary Haskell code.) I hope there’s a way to either (a) preserve a simple notation like “fst” rather than “proj1 proofA proofB” or (b) automatically synthesize the proof arguments in a general/parametric enough way to allow a multitude of interpretations. I suppose I could instead replace the single generalizing GHC plugin with a number of plugins that produce different specializations of a single theoretical generalization. Wouldn’t be as elegant, though. BTW, have you see the new paper *The constrained-monad problemhttp://www.ittc.ku.edu/csdl/fpg/papers/Sculthorpe-13-ConstrainedMonad.html *? I want to investigate whether its techniques can apply to Category & friends for linear maps and for circuits. Perhaps you’d like to give it a try as well. I got to linear maps as an elegant formulation of timing analysis for circuits. I’m glad you liked the “Reimagining Matrices” post! It’s a piece of a beautiful tapestry that leads through semirings, lattices, categories, and circuit analysis. I hope to back to writing soon and release another chapter. Encouragement like yours always helps my motivation. Regards, - Conal On Thu, May 9, 2013 at 7:05 AM, Sjoerd Visscher wrote:

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe