Add constraints to (&&&) and terminal

[ryantrinkle]

This allows the author of a category to control which objects can be duplicated or destroyed

Feedback would be very welcome! There were a few spots I had to fix up that I didn't really understand.

[ryantrinkle]

The one thing that looks quite wrong to me is https://github.com/leftaroundabout/constrained-categories/pull/4/files#diff-d0d577734d6e315b83e3b0c919c88b8b3f31d380b8ccc5a0bf87cf511bcdf051R280 . I wasn't sure how to get rid of this.

[leftaroundabout]

Thanks for the contribution!

Could you give an example category where these constraints are needed? (I don't doubt that there are such categories, just would like to look at it and get a feel if the constraints can maybe be introduced elsewhere that would lead to less signature-bloat.)

[emeinhardt]

Plausibly anything modeling linear phenomena at the type-level --- whether that's trying to model some kind of linear types, something more related to intuitionistic logic, concatenative languages (or some other reason for looking at linear-flavored combinatory logic), or some domain (maybe some kind of optimization problem) where 'linearity' is transparently modeling something like a resource.

One example domain (I'd have to work through the idea more to be more confident about exactly where this would show up in Haskell) would be any categorical model closely related to formal language and automata theory (could be a more academic library literally about those topics, or a generalized one about (not-necessarily-finite) state machines, or a similar one for parsing, or a similar one for recursion schemes) where there are 'linear' flavored constraints that can be an important lens for understanding different models of computation with different degrees of expressivity (and with accompanying trade-offs in a programmer's and compiler's ability to do static analysis). I'm happy to elaborate with examples/citations --- some even have Haskell or at least math mostly with abstractions that a Haskeller may find familiar.

Stuff useful for this topic is plausibly likely to line up or be closely related to other things Haskellers are likely to want to model or implement, including parsers and recursion schemes that provide a finer-grained version of the kinds of trade-offs that e.g. cause people to reach for Applicative (or Selective or Arrow or ...) parsers instead of Monadic ones.

[leftaroundabout]

@emeinhardt sounds intriguing. I'm happy to merge this if it has a concrete use case, as long as it doesn't introduce an unnecessary amount of complexity to the signatures.

And I don't have a lot of time currently.

[emeinhardt]

So besides categorical logic, another example that would motivate these constraints (and/or elaborating the hierarchy of monoidal categories): Markov categories.

[leftaroundabout]

@emeinhardt cool. You have an implementation of that which needs the patch?