[TYPES] effect vs. coeffect expressiveness

[Aleksandar Nanevski]

Hi Jonathan.

In my PhD thesis (CMU 2004), I have considered the distinction between 
different kinds of effects using types from (contextual) modal logic S4. 
In S4 one has two different type constructors, Box (universal quantifier 
over possible worlds) and Diamond (existential quantifier). Computations 
with a Box type are ones that depend on the environment but don't change 
it. Box is a comonad. Computations with a Diamond type are ones that 
change it. Diamond is a monad.

https://software.imdea.org/~aleks/thesis/CMU-CS-04-151.pdf

The results in the thesis were based on the following papers and TR's. 
For example, this TR discusses that exceptions (and other control-flow 
effects such as delimited continuations) should be viewed as Box-ed 
(i.e., comonadic) computations

https://software.imdea.org/~aleks/papers/effects/CMU-CS-03-149.pdf

This paper discusses that state can be viewed as a Diamond (i.e., 
monadic) computation, but if one views it as a Boxed (comonadic) 
computation, then one still gets something familiar, namely, dynamic 
binding. The two kinds can also nicely interact in one and the same 
calculus.

https://software.imdea.org/~aleks/papers/effects/possibility.pdf

Another way to view these two different kinds of computation as follows. 
Once you put a contextual information onto the boxed type, that 
information serves as a *precondition* for your program. Once you put 
contextual information onto the diamond type, it serves as a 
*postcondition*. Having both together in a same system gives you Hoare 
Type Theory (in fact, a type-based version of separation logic), which 
is something that I worked on as a postdoc:

https://software.imdea.org/~aleks/papers/hoarelogic/htt.pdf

https://software.imdea.org/~aleks/papers/hoarelogic/icfp06.pdf

I hope you find these pointers useful.

Best regards,

Aleks


On 30/04/2020 01:48, Jonathan Aldrich wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear Types,
>
> I am curious about the relative expressiveness of effects and
> coeffects.  Has this been studied?
>
> The cleanest distinction I've seen is that effects capture the impact
> a program has on its environment, i.e. what it produces.  Coeffects
> capture the requirements that a program puts on its environment: what
> it consumes.  This is discussed, for example, in Gaboardi et al's ICFP
> 2016 paper, "Combining Effects and Coeffects via Grading" (and
> elsewhere).
>
> There is some useful intuition in this distinction, and it describes
> the different structure of checking rules in effect and coeffect
> systems.  However, I don't find this distinction very helpful in
> thinking about expressiveness.  It seems like many examples can be
> expressed in either an effect or a coeffect system.  For example, an
> exception is a classic example of an effect (e.g. in the paper
> mentioned above, and many others).  However, it seems to me that
> exceptions can also be modeled as coeffects: code that might throw an
> exception requires the caller to pass a handler for that exception to
> it--or perhaps an abstract "permission" to throw that exception.  So
> in what sense are exceptions an effect, rather than a coeffect?
>
> Is this true of all the kinds of things that are typically expressed
> with effects and coeffects--that they could just as easily be
> expressed in the other style?  If so, what are the benefits of one
> style vs. the other?  Or are there examples that can only be expressed
> in one style--or for which expression in the other style is much more
> awkward?
>
> Perhaps these questions have been written about, but I haven't been
> able to find it.  I would love to get some pointers.  I am
> particularly interested in a practical explanation of the differences
> in expressiveness, or theoretical results that have a direct and
> explicit relationship to practice--with practical examples in either
> case.  (co-)Monads and/or anything categorical are not a very helpful
> starting point for me, but effect systems and/or linear types are
> (I've done research on both).  I am also more interested in the
> descriptive view of effects/coeffects (in the sense of Filinski,
> ICFP'11) than the prescriptive view.
>
> Thanks,
>
> Jonathan