[TYPES] effect vs. coeffect expressiveness

[Ralf Jung]

Hallo Neel,

(This is moving away from effects and coeeffects a bit, I hope that is okay.)

> How should tensor products and computations interact? Well, we
> know that the monad and tensor should satisfy the property of
> having a *strength*:
> 
>     strength : T(C, X) ⊗ Y ⊸ T(C, X ⊗ Y)
> 
> Surprisingly, having a linear strength corresponds to the *frame
> property* of separation logic. Intuitively, if you think of
> 
>     f : P ⊸ T(C, Q)
> 
> as representing a computation that has a precondition `P` and
> postcondition `Q`, then having a strength is what you need to
> derive
> 
>     g : P ⊗ R ⊸ T(C, Q ⊗ R)
> 
> You can see it with the following linear term:
> 
>     frame : (P ⊸ T(C, Q)) ⊸ (P ⊗ R) ⊸ T(C, Q ⊗ R)
>     frame f (p, r) = strength(f p, r)
> 
> I documented this relationship in my POPL 2015 paper, *Integrating
> Linear and Dependent Types*, but I think it was folklore before that:
> Bob Atkey mentioned to me that he knew it as well.  In addition, I
> should note having a strength with the tensor is what is needed to
> make the linear version of do-notation work out the way that you
> expect.

Indeed we (later, independently) made the same observation for the laws of our
"update modality" in Iris [0], where I wrote a rule like your "strength" above
but called it "framing" (not knowing monad terminology), and then someone
pointed out the connection to me.

[0]: https://www.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf

> Now, two surprising things happen. 
> 
> First, in this setting, there is a natural notion of nonlinear arrow
> which **is not** the linear decomposition `!A ⊸ B`. Instead, there is
> a free-standing function space `A → B` which represents a function
> which can *share* capabilities with its argument, just like the
> ordinary implication in separation logic permits sharing resources
> between hypothesis and consequent.

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.

> Indeed, this notion of function type corresponds to *capability-safe
> functions* -- these are functions which can only access capabilities
> either through their argument or their free variables. That is, they
> are functions which *lack ambient authority*.

This is very interesting.  While we *have* both magic wand and implication, we
don't actually use implication in Iris.  (We do use the fact that existentials
commute with conjunction, which implies the existence of implication, but that's
it.)  We only use magic wand.  Both are equivalent in some situations (but this,
I think, relies on the fact that Iris is linear and not affine), which is why
you might see implications in our papers, but really we only do that to
hopefully not confuse the reader with too many magic wands.  This is in contrast
to the conjunctions, where we do use both of them in meaningful ways.

So in your context of doing this with a linear programming language, do you have
an example where implication is actually *useful*?  As you mention above, these
functions can access their arguments *or* their environment, but not both, which
seems rather restrictive.  (I do not understand what you mean by "lacking
ambient authority".)

Kind regards,
Ralf