[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Jonathan,
There is not much more written as there is a lot that we do not
understand here. I will present my point of view on the subject (this is
an invitation for other point of view to express themselves ;).
First of all, I may have been attracted by the production/consumption
distinction, I do not use it anymore. It is miss-leading and not that
usefull as you said.
One thing is certain : monads are way more natural in call-by-value, and
comonads are way more natural in call-by-name. I have to stop Haskeller
complaints as an aparte : most monad in Haskell are intrincically CbV as
the argument is evaluated to some extent by the bind, in addition
Haskell is call-by-need, which is slightly different from this point of
view.
The real distinction I use on effects/coeffects is related to this
statement : *effects describe what happen when the piece of code is
evaluated*, while *coeffects describe what append when it is manipulated
*(copied/erased/distributed).
Following this idea, one can see that most coeffects can be somehow
encapsulated into effects (basically by looking at what happened to the
other copies of the codes); and worst, all applied coeffect on the
literature are internally encoded this way since code manipulations are
not accessible by programmers. But I believe that there is more to be
discovered and used from coeffect, especially for writing concurrent
programs or performing code analyses.
I was a bit expeditious, I can develop some of the points if you are
interested.
I hope you enjoyed those random thoughts, and I invite other to do the
same. This subject is very interesting, but too fuzzy for it to be
formalized yet :)
Cheers,
Flavien (the one from Gaboardi et al's ICFP paper)
Le 30/04/2020 à 01:48, Jonathan Aldrich a écrit :
[ 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
