[TYPES] effect vs. coeffect expressiveness

[O'Hearn, Peter]

On 1 May 2020, at 11:57, Ralf Jung <jung at mpi-sws.org<mailto:jung at mpi-sws.org>> wrote:

In Iris, being a separation logic, we also have both magic wand and implication.
I have long wondered about the connection to linear logic and was quite
surprised when I realized that the "implication" in linear logic (`!A ⊸ B`) does
not correspond to our implication in Iris.  Ever since then I wonder why
implication in linear logic looks the way it does.

Hi Ralf, the difference between BI and LL was explained in the very first paper on BI by Pym and I: see the last section of http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/BI.pdf .  SL inherits the differences.

The most important point (IMHO) is that if you take a semantic perspective, then the difference jumps out so should not be surprising. And I think looking at the models explains “why” each of the implications is like they are: they flow inevitably from natural models.

In essence,
 — BI corresponds to a single category possessing both a monoidal closed (so, -*) and a cartesian closed (so, ->) structure **in the same category**. Naturally occurring model: presheaves over a symmetric monoidal category of worlds (like in separation logic, or rather Day’s pro-monoidal structure).
 — (intuitionistic) LL is semantically two categories, one monoidal closed and the other cartesian closed, with an adjunction between them (which gives you !). So yes two closed structure (two implications), but **not for the same category**. Naturally occurring model: coherence spaces and linear maps as SMCC, coherence spaces and stable maps as CCC (I hope I remember correctly). You can also choose to induce the second category as the Klesli category of a comonad, but I find the “two categories” model more natural.

BI also has a natural Kripke truth-functional semantics which you are used to, but I have always drawn LL intuition not from a truth-functional semantics but from its lovely semantics of proofs (like coherence spaces).

The LL monoidal closed category is usually not also cartesian closed. E.g., coherence spaces and linear maps case.

There is no value judgement in these models: the two systems just fit their models very naturally, and the models occur in nature. If you don’t have one of these models in your hands, no problem, no need to apply a shoehorn. Anyhow, once on sees the semantics of BI and LL in these terms, I hope it is not surprising that LL does not “have” -> (if you are sitting in the monoidal category, like you are the way LL is usually formulated).

You can replace “monoidal closed category” by “residuated monoid” and CCC by “heyting algebra” for a non-categorical explanation of the above.

My paper “On bunched Typing” (http://www.cs.ucl.ac.uk/staff/p.ohearn/papers/BunchedTyping.pdf)  contrasts they systems’ views of shared versus consumable resources (in old OS terminology); i.e., using types instead of models.

best,  Peter