[TYPES] effect vs. coeffect expressiveness

[Dominic Orchard]

Dear Jonathan,

This is a great question and something that I think still lacks a thorough
comprehensive treatment in the literature, but certainly there are hints
about this in various places (and I have been slowly feeling my way towards
different versions of this question, including some work in progress right
now!)

This is certainly something that we are trying to explore in the Granule
project (https://granule-project.github.io/, and at ICFP 2019) where we
have a fully functioning modern functional programming language which can
work with various different effects and coeffects at the same time. We are
brewing a few things comparing certain analyses performed as effects vs
coeffects (because, as you say, it seems that some things can be done both
ways, so why choose one over the other?). It's probably worth pointing out
that, whilst there is quite a bit of recent work with coeffects in a linear
type theory (like Granule and the ICFP 2016 paper you mention), coeffects
need not be tided to a linear type theory (indeed, the first two papers
that Tomas, Alan, and I wrote on this were in a Cartesian setting (ICALP
2013 and ICFP 2014)).

My general, informal view is that (broadly) monadic effects capture a kind
of 'forwards' analysis, with information flowing from inputs to outputs,
whereas comonadic coeffects capture an 'backwards'-style analysis, flowing
back through the inputs. How you structure the primitives for working with
either will affect how easy it is to capture certain properties (and the
CBN/CBV story then becomes important as well, see the Cicek et al. paper
mentioned below).

Here are a few references that spring to mind that go a little bit towards
your question:

* Tomas Petricek and I reflected on coeffect vs effect expressivity a bit
in Section 8 of this paper (
https://www.cs.kent.ac.uk/people/staff/dao7/publ/haskell14-effects.pdf)
where we give a brief comparison between expressing implicit parameters as
effects vs coeffects (reader graded monad vs product graded comonad) and
what the difference is (we point out that Haskell's implicit parameters
feature are a coeffect rather than an effect, perhaps the most "mainstream"
example of explicit coeffects in the wild!).

* This short paper by Ezgi Cicek, Marco Gaboardi, and Deepak Garg looks at
this question in the context of cost analysis (
https://lipn.univ-paris13.fr/DICE2016/Abstracts/paper_10.pdf).

* I know that you said a (co)monad treatment is not helpful to you, but in
case it helps others, I have this unpublished article from the end of my
PhD "Should I use a Monad or Comonad?" which at least explains some overlap
(
https://www.cs.kent.ac.uk/people/staff/dao7/drafts/monad-or-comonad-orchard11-draft.pdf)
and tries to reconcile some tensions in the literature. The paper is meant
to be a fairly self-contained.

* The ICFP 2018 by Andrew Hirsch and Ross Tate (
http://www.cs.cornell.edu/~ross/publications/sleffects/sleffects-icfp18-tr.pdf)
is not quite what you are after but certainly has interesting things to say
about connecting monadic effects and comonadic coeffects.

Hope those help. I would be interested in having a further conversation
about this sometime if you want to grab a Skype call.

Best,
Dominic

On Thu, 30 Apr 2020 at 07:24, Jonathan Aldrich <jonathan.aldrich at cs.cmu.edu>
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
>