[TYPES] effect vs. coeffect expressiveness

[Marco Servetto]

Hi,
Citing Michael
"This involves associating information with the context – namely how
each variable is used – so it is in essence a coeffect system."
This indeed seams to confirm my general understanding:
effects are computed\inferred
coeffects are checked
So, is every kind of "type environment" is a form of a coeffect? in
that case, here we have the answer to the question of Jonathan:
Lets consider one of the simplest and most famous type systems: the
simply typed lambda calculus.

We can encode the type of variables in an environment Gamma
(x1:T1..xn:Tn) and we can get the simple and elegant type system we
all known.

OR we can make a complex system of constraints and we can have a
Judgment of the form |-e: <T ; Gamma>
and we would type the lambda abstraction
               |-e :<T:Gamma>
----------------------------------------------------
  |-   \x:T1.e : < T1->T  : Gamma[x=T1] >
Then, depending on how we define types T, Gamma and Gamma[x=T] we
would either have a mathematically equivalent version of the
conventional system but "wrote funny"
or a highly generic type system where the type needed for local
variables is expressed as constraints and Gamma[x=T1] is adding more
constraints (possibly triggering a simplification-minimization of the
current constraint set)
In general, you get a form of type inference from effect systems:
Imagine if such simply typed lambda calculus was to ALSO support an
"untyped" lambda \x.e; with an effect type system, such lambda term
would be able to work as a "generic method". On the other side,
effects tend to be much harder to define\compute then simply checking
information readily available in an environment.

Going back to the original case of the exceptions: if all the methods
define what exceptions they are allowed to leak, then effects are
redundant effort.
On the other side, if we wanted to infer what exceptions a method can
throw, in the same way the simply typed lambda calculus infers the
return type of lambda terms, then effects would be perfect for the
task.

Marco!

On Fri, 1 May 2020 at 09:04, Michael Arntzenius <daekharel at gmail.com> wrote:
>
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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
> > >
> >