<div dir="ltr"><blockquote>
</blockquote><p>Hi Sjoerd,</p>
<p>Thanks very much for the help sorting out options for more
flexibility in Category instances. I like how you spotted and removed
the <code>id</code> problem.</p>
<p>I’ve <a href="https://gist.github.com/conal/5549861">cloned your gist</a> and tried out an idea to simplify verifying the required constraints on linear map values.</p>
<p>About the change from <code>a ⊸ b</code> to <code>LM s a b</code>, I originally used the latter style (as a scalar-parametrized family of categories, using the explicit <code>s</code> parameter to <code>VS</code>, <code>VS2</code>, etc), but I greatly prefer the former notation, especially when type-set. I guess with lhs2tex, we could typeset “<code>LM s a b</code>” by placing the “s” under the (multi)linear map symbol or some such, or perhaps even omit it.</p>
<p>Am I right in thinking that the first two (<code>Obj</code>) arguments <code>proj1</code> and <code>proj2</code> serve as proofs that the types involved are legitimate for the category (<code>k</code>)?</p>
<blockquote>
</blockquote><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"><p>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 <code>fstL</code> and <code>sndL</code> in the gist.</p></blockquote><blockquote>
</blockquote>
<p>I wonder whether this trick is compatible for my goals with circuit
synthesis and analysis. I want to express fairly general computations
over <code>Category</code> 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 “<code>fst</code>” rather than “<code>proj1 proofA proofB</code>”
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.</p>
<p>BTW, have you see the new paper <em><a href="http://www.ittc.ku.edu/csdl/fpg/papers/Sculthorpe-13-ConstrainedMonad.html" title="paper by Neil Sculthorpe, Jan Bracker, George Giorgidze, and Andy Gill (submitted to ICFP 2013)">The constrained-monad problem</a></em>? I want to investigate whether its techniques can apply to <code>Category</code>
& 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.</p>
<p>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.</p>
<p>Regards, - Conal</p><blockquote>
</blockquote></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, May 9, 2013 at 7:05 AM, Sjoerd Visscher <span dir="ltr"><<a href="mailto:sjoerd@w3future.com" target="_blank">sjoerd@w3future.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Hi Conal,<div><br></div><div>I have a package data-category that should be able to do this. </div>
<div><a href="http://hackage.haskell.org/package/data-category" target="_blank">http://hackage.haskell.org/package/data-category</a></div><div><br></div><div>I tried implementing your linear map, and this is the result:</div>
<div><a href="https://gist.github.com/sjoerdvisscher/5547235" target="_blank">https://gist.github.com/sjoerdvisscher/5547235</a></div><div><br></div><div>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:</div>
<div><br></div><div>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!</div>
<div><br></div><div>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.</div>
<div><br></div><div>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. </div>
<div><br></div><div>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.</div>
<div><br></div><div>Because of the requirement that every value is a valid arrow, there's no need to change the definition of composition.</div><div><br></div><div>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.</div>
<div><br></div><div>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.</div>
<div><br></div><div>I hope this helps you implement your ideas further. Your reimagining matrices post was really superb and I'd love to learn more!</div><div><br></div><div>greetings,</div><div>Sjoerd</div><div><br>
<div>
<div class="im"><div>On May 8, 2013, at 12:09 AM, Conal Elliott <<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>> wrote:</div><br></div><blockquote type="cite"><div class="im"><div dir="ltr"><div>
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?<br>
<br></div>Thanks, -- Conal<br></div></div>
_______________________________________________<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br><a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br></div></div></blockquote></div><br></div>