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 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 s parameter 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 proj2 serve 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
fstLandsndLin 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 problem? 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
Hi Conal,I have a package data-category that should be able to do this.I tried implementing your linear map, and this is the result: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@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe