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

[Conal Elliott]

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 <sjoerd at 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 <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/baf78bf5/attachment-0001.htm>