Re: [TYPES] effect vs. coeffect expressiveness

[ 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