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 problem<http://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 <sjo...@w3future.com> 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 <co...@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 > > >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
