Distributivity of ! over?

Question

Has anyone studied a variant of linear logic, or of its semantic counterpart (exponential modalities on linearly distributive categories / $\ast$-autonomous categories / polycategories) for which there is a distributive law

$$!? \to ?!$$

Presumably it would need to interact sensibly with the (co)monoidal structure of ! and ?. I haven't thought about whether there is a nice sequent calculus or resource interpretation. I ask for two reasons:

1. Such a distributive law should imply that there is a "mixed Kleisli category" whose morphisms from $A$ to $B$ are the morphisms $!A \to ?B$. This would be more symmetrical and pleasing than the usual translation of classical logic involving morphisms $!?A \to ?B$.

2. In $\rm Chu(Cat,Set)$ I believe there is such a distributive law, or at least a pseudo-distributive law, and a morphism $!A\to ?B$ should be precisely a profunctor from $A^+$ to $B^-$. So this would give a nice way of recovering $\rm Prof$ from $\rm Chu(Cat,Set)$.

Answer 1

I would tend to say "no".

However, besides my comment above, which is not very pertinent, let me mention the paper Combining effects and coeffects via grading, by Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart and Tarmo Uustalu. They consider "graded" monads and comonads, which include usual monads and comonads as the special case in which the grading is trivial (I don't know who introduced these first, I learned of graded comonads from this note by Paul-André Melliès). The programming language underlying their work is linear and their comonads are graded in a semiring (rather than just a monoid) so that they are a generalization of the exponential modality $!(-)$ of linear logic (the additive structure of the semiring grades weakening/contraction, i.e. the monoidal structure of the comonad, while the multiplicative structure of the semiring grades the actual comonad structure, i.e., the counit and the comultiplication). They then study graded versions of the usual distributive law between monads and comonads in order to account for the simultaneous presence of "quantitative" effects and coeffects in programming languages (e.g., not just tell whether a program may raise an exception but tell, if possible, how many exceptions it will raise, or whatever. This is what the increased expressiveness given by the grading is meant to be used for).

So, forgetting the grading, i.e., if we grade everything with the trivial semiring and the trivial monoid, we are close to what you describe, but not quite: while the trivially graded version of their comonad is, indeed, the $!(-)$ modality of linear logic, the $?(-)$ modality does not fit into their axiomatization, because the trivially graded version of their monad is necessarily strong, and $?(-)$ is not a strong monad. So, strictly speaking, this work says nothing about the distributive law you are looking at.

I skimmed through the references given by Gaboardi et al. in relation with distributive laws and none of them seems to mention linear logic. This supports my belief that no one has ever introduced/studied the variant of linear logic you mention... but of course I can't be sure!