Conal Elliott | 8 May 00:09 2013
Picon

Constrained Category, Arrow, ArrowChoice, etc?

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
Sjoerd Visscher | 9 May 16:05 2013

Re: Constrained Category, Arrow, ArrowChoice, etc?

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 <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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Conal Elliott | 9 May 22:36 2013
Picon

Re: 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 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 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? 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. 

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 <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


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Sjoerd Visscher | 10 May 00:03 2013

Re: Constrained Category, Arrow, ArrowChoice, etc?

Hi Conal,

I’ve cloned your gist and tried out an idea to simplify verifying the required constraints on linear map values.

Lovely use of view patterns! It looks like it is not necessary to store the LM value, all that is needed is to store that VS2 s a b is satisfied.

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)?

Yes, that's one of the reasons. The other reason is that BinaryProduct is a type family, so it is not possible to derive from the product what it originally was a product of. For example in the Boolean category with the false and true objects and an arrow from false to true, the binary product is conjunction, and there are multiple combinations that give the product false.
https://github.com/sjoerdvisscher/data-category/blob/master/Data/Category/Boolean.hs

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.

I'd go for (b). The proofs are just identity arrows, so you can usually use the src and tgt methods to retrieve them generically. I don't expect problems there.

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 scanned through it and was quite impressed. Definitely something to dive deeper into.

greetings,
Sjoerd
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Sjoerd Visscher | 10 May 17:20 2013

Re: Constrained Category, Arrow, ArrowChoice, etc?


On May 9, 2013, at 10:36 PM, Conal Elliott <conal <at> conal.net> wrote:

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 have implemented the normal form for categories. The normal form is like the type-threaded lists from the thrist package:

Evaluating the normal form works fine even for your original :-* datatype.

But I got stuck trying to expand this to categories with products, as I'm not sure what the normal form should be. But I guess you might have good ideas about that?

Sjoerd
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane