"Generalized arrows" and proc notation?

Question

When learning about Control.Arrow and Haskell's built-in proc notation, I had the idea that this language might prove very useful as an eDSL for general monoidal categories (using *** for tensor and >>> for composition), if only the Arrow typeclass were generalized to allow a general tens :: * -> * -> * operation rather than Arrow's (,) : * -> * -> *.

After doing some research, I found GArrows, which seem to fit my needs. However, the linked Garrow typeclass comes bundled with the so-called "HetMet" GHC extensions, and support for other features that (for the time being, anyway), I don't have much use for, such as "modal types".

Given that I would like to be able to use such a GArrow typeclass without having to install non-standard GHC extensions:

1. Is there an actual (somewhat standardized) library on Hackage that meets my needs for such a generalized arrow typeclass?

2. Given such a library, is there any way to use such a GArrow type class with a "generalized proc" notation without having to cook up my own GHC extension? (With RebindableSyntax perhaps?)

Note: Also, I'm fine with using quasiquotation for a generalized proc notation. So perhaps it wouldn't be too difficult to modify something like this to suit my needs.

Vang

Have you found anything suitable in the meantime, or an alternative approach? In case I haven't made it clear enough yet: I'm very interested in this too, both the category stuff in general but also the music application in particular. If I can help in some way, don't hesitate to tap me on Github. Maybe we can fork constrained-categories if it helps. – Cinchona

@Cinchona I've been working on this a bit on and off. The biggest issue for me so far has been getting a nice type class hierarchy for different kinds of monoidal categories. To be completely general, I want to have a category typeclass like this, which I don't think is very easy to accomplish in Haskell without a ton of compiler extensions. – Vang

gist.github.com/leftaroundabout/… – Cinchona

Answer 1

I've wondered about that before, too. But – proc notation is so widely considered a silly oddball that there's probably not much interest in generalisation either (though I daresay this is what would make it actually useful!)

However, it's actually not necessary to have special syntax. The primary reference that must be named here is Conal Elliott's work on compiling lambda notation to bicartesian closed categories. Which I thought would have caught on in the Haskell community some time by now, but somehow hasn't. It is available as a GHC plugin, at any rate.

Even that isn't always needed. For some category combinators, you can just wrap a value that's universally quantified in the argument, and treat that as a pseudo-return-value. I call those Agent in constrained-categories; not sure if that's usable for your application, at any rate several things you'd do with arrow-like categories can be done. (In constrained-categories, the tensor product is fixed to (,), however, so probably not what you want. Although, could you explain what tensor product you need?)

Cinchona

I'm currently working on a library for preforming various transformations (e.x. translations, transpositions, retrograde inversion, etc...) on abstract representations of musical scores. I haven't settled on the data type to use for this yet, but I'm pretty sure I need something more general than (,). Or at least I think it would be nicer with something more general. (I'm thinking of using some variation on sized vectors of this, since e.x. I need to keep track on how many lines there are in a score, and I would like to be able to express this at the type level) – Vang

So, I think (,) actually would work for my particular application, in that a is isomorphic to Vec 1 a, (a,a) is isomorphic to Vec 2 a, ((a,a),a) isomorphic to Vec 3 a and so on. But this doesn't seem as clean as using typed vectors, and I'd also like to potentially consider other monoidal categories in the future. – Vang

Yeah. The reason I stayed with (,) in constrained-categories is that a) in many interesting categories, this can indeed be used just fine (I suspect this could somehow be explained with the Yoneda lemma) and b) it helps type inference. But yeah, proper associativity of the tensor product would certainly be nice conceptually; it would actually make type inference more difficult though. – Cinchona