[TYPES] effect vs. coeffect expressiveness

[Michael Arntzenius]

Dear Jonathan,

> Or are there examples that can only be expressed
in one style--or for which expression in the other style is much more
awkward?

I was about to conjecture that I had an example of something that could
only be expressed as a coeffect, but reading Dominic's reply I've realized
I was wrong. I still offer it, though, as a concrete example of something
that I think would be more awkward to express as an effect:
non-monotonicity in an otherwise monotone world. I can only hope this isn't
too obscure to be interesting :).

The gist here is that, if we assign each of our types a partial order, and
track for each function whether it is monotone with respect to this order
or not in its type, then we can determine for each variable used in an
expression whether it is used monotonically or not. This lets us track
monotonicity in our type system. This involves associating information with
the context – namely how each variable is used – so it is in essence a
coeffect system.

For full details you can read the ICFP 2016 paper "Datafun: A Functional
Datalog". (This doesn't mention coeffects explicitly; I didn't notice the
connection at the time.) I believe this is also similar to how
variance/positivity checking in proof assistants works.

It is also possible to express this as an effect, following the recipe laid
out in “Should I use a Monad or Comonad?”. To do this, interpret our types
as pre-ordered instead (i.e. drop the requirement that a type's order is
antisymmetric). Then a non-monotone map A -> B can be represented by a
monotone map A -> indisc B, where "indisc" is the "indiscreteness monad",
which makes (x <= y : indisc B) always true! So this makes non-monotonicity
into an effect; in essence, purity = monotonicity, impurity =
non-monotonicity.

But this approach makes working with functions that are monotone in some
but not all arguments awkward. For example, a function f : A -> B -> C that
is monotone in B but not A must be typed A -> indisc (B -> C). This is not
equivalent to A -> B -> indisc C, which does not guarantee monotonicity in
B. From an effect-based POV, the former requires the "effect" to occur
before the function has even seen the value of type B. With most effects we
rarely care about details like this, but in Datafun we care a lot. So for
our use case, I think a context-oriented coeffect view is more convenient
for the programmer.

In wonder if this generalizes? Perhaps, if you find yourself working with
values of type T(A -> B) often, where T is a monad, it might be more
convenient to work with an equivalent coeffect system instead, should one
exist.

Cheers,
Michael Arntzenius

On Thu, Apr 30, 2020 at 18:14 Dominic Orchard <dom.orchard at gmail.com> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> 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
> >
>