Capabilities and Effects

84 views
Skip to first unread message

Will Sargent

unread,
Jul 3, 2018, 1:42:20 PM7/3/18
to <friam@googlegroups.com>
Hi all,

There's a couple of papers I've been reading as I'm digging into capabilities and effects.  


> Capabilities and effects are two sides of the same coin. Capabilities are prescriptive, while effects are descriptive, but that is only a matter of presentation. (I do find the capability view somewhat more inspiring.

The only other paper I can find on capabilities and effects specifically is this one:


It seems like this is something I can sell much easier as a shift in perspective to the FP crowd -- does anyone know of any other papers or literature on the subject?

Thanks,
Will.

Will Sargent

unread,
Jul 3, 2018, 1:46:56 PM7/3/18
to <friam@googlegroups.com>
Answering my own question: François Pottier (guy who wrote that paper) has a bunch of talks and papers:



Also Arthur Charguéraud:


Mark Miller

unread,
Jul 3, 2018, 8:06:15 PM7/3/18
to fr...@googlegroups.com
On Tue, Jul 3, 2018 at 10:46 AM Will Sargent <will.s...@gmail.com> wrote:
Answering my own question: François Pottier (guy who wrote that paper) has a bunch of talks and papers:



Also Arthur Charguéraud:





On Tue, Jul 3, 2018 at 10:41 AM, Will Sargent <will.s...@gmail.com> wrote:
Hi all,

There's a couple of papers I've been reading as I'm digging into capabilities and effects.  


> Capabilities and effects are two sides of the same coin. Capabilities are prescriptive, while effects are descriptive, but that is only a matter of presentation. (I do find the capability view somewhat more inspiring.

The only other paper I can find on capabilities and effects specifically is this one:


It seems like this is something I can sell much easier as a shift in perspective to the FP crowd -- does anyone know of any other papers or literature on the subject?

Thanks,
Will.

--
You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.
To post to this group, send email to fr...@googlegroups.com.
Visit this group at https://groups.google.com/group/friam.
For more options, visit https://groups.google.com/d/optout.


--
  Cheers,
  --MarkM

Matt Rice

unread,
Jul 4, 2018, 12:36:33 AM7/4/18
to fr...@googlegroups.com
On Tue, Jul 3, 2018 at 10:41 AM, Will Sargent <will.s...@gmail.com> wrote:
> Hi all,
>
> There's a couple of papers I've been reading as I'm digging into
> capabilities and effects.
>
> Notably in this slide deck, around slide 39:
> http://pauillac.inria.fr/~fpottier/slides/fpottier-2007-05-linear-bestiary.pdf
>
>> Capabilities and effects are two sides of the same coin. Capabilities are
>> prescriptive, while effects are descriptive, but that is only a matter of
>> presentation. (I do find the capability view somewhat more inspiring.

Here is another,

A Study of Capability-Based Effect Systems:
https://infoscience.epfl.ch/record/219173/files/thesis-2017-1-update_1.pdf

And perhaps i should quibble that i'm not so sure about the above
quote that it is merely a matter of presentation,
I think that while type & effect systems certainly have more cognitive
load, trust is placed differently,
in e.g. the KeyKOS factory, the implementation of the factory is trusted,
and you dynamically check that the factory was created by a trusted
factory creator.

whereas type & effect systems place the trust in the type checker
leaving a factory implementation trusted solely because it is checked,
which allows you to parley trust into a 3rd party factory
implementation of untrusted origin.

the thought here is that perhaps in KeyKOS factory, you could create
two factories communicating bidirectionally via the "hole"
and perhaps with type & effect systems, you get consensus between
parties of exactly what capability goes in the hole, (which you can
probably get with revocation/ask bob with the keykos factory/hole)

In the *-Property there is the notion of a capability filter, which
filters various capabilities, type & effect systems have this built in
via
adding tagging of effects on top of the existing type tagging of data,
where capability systems merely tag effects

Perhaps merely presentational, but I at least have an easier time
thinking about bidirectional forms of factories and the *-property in
type & effect systems,
while perhaps the common cases of a single domain, are more difficult
(and easier in a capability system).
To the extent that i wonder if there are not minute differences in
practice if not quantitatively.

> The only other paper I can find on capabilities and effects specifically is
> this one:
>
> http://homepages.ecs.vuw.ac.nz/~alex/files/CraigPotaninGrovesAldrichOCAP2017.pdf
>
> It seems like this is something I can sell much easier as a shift in
> perspective to the FP crowd -- does anyone know of any other papers or
> literature on the subject?
>
> Thanks,
> Will.
>

Will Sargent

unread,
Jul 9, 2018, 8:15:34 PM7/9/18
to <friam@googlegroups.com>
This is really great -- he also has a github reference:


and superficially it looks like Scala with some bits added on top, like Wyvern.


> To post to this group, send email to fr...@googlegroups.com.
> Visit this group at https://groups.google.com/group/friam.
> For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+unsubscribe@googlegroups.com.

fengyun liu

unread,
Jul 11, 2018, 12:16:44 PM7/11/18
to friam
Thanks to Will for pointing me to this exciting group.

The repo above is a little outdated. In the attached (rejected) draft, we've made a little theoretical progress by semantically reasoning about memory effects with stoic functions based on step-indexed logical relations. It turns out in the thesis, we take for granted for some typing rules, which will not work with memory effects. In particular, the following rule doesn't hold in the presence of mutation:

pure(Γ) ⊢ t : T1 ⇒T2

----------------------------             (A)

 Γ ⊢ t : T1 →T2


For soundness, we need to restrict that the term t is a value:

pure(Γ) ⊢ v : T1 ⇒T2

----------------------------             (B)

 Γ ⊢ v : T1 →T2


The rule (A) is problematic for effects as it invalidates safe optimization (an important usage of effect system), but I conjecture it may have some application in the setting of security. But I don't understand much about security, so I don't pursue that direction currently. I'm keen to learn more from the group about the interplay of PL, effects, capabilities, and security.

Cheers,
Fengyun

> To post to this group, send email to fr...@googlegroups.com.
> Visit this group at https://groups.google.com/group/friam.
> For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.
stoic.pdf

Will Sargent

unread,
Jul 16, 2018, 8:08:44 PM7/16/18
to <friam@googlegroups.com>
More about capabilities vs effects from Martin Odersky:


Let's do a thought experiment. Instead of having a "magical" IO monad, let's have a magical capability CanIO. Then, instead of returning an IO[T], a function would instead return a CanIO => T. So this says "give me the capability to do IO and I return a T". Assume the CanIO capability is produced only by the runtime that executes a program. Then every program and every function that has side effects has to be of type CanIO => T, since there is no other way to get the capability. This is exactly the effect of an IO monad. However, instead of opaque IO components which are cobbled together with cumbersome monad operations, you now have regular functions that you can compose functionally! No more pains to express recursion, need to trampoline, and so on.

To avoid boilerplate, you want to make the capability parameter implicit and abstractable; that's exactly what Scala 3's implicit function types are about (to find out more: google for "Simplicitly, POPL 2018"). In the end, this gives you a system that can run exactly like a regular side-effecting system, except at each step the types tell you whether something belongs to the pure or the effectful half. Also, pure and effectful functions are composed in the same way, no more need to go monadic, no need to do monad transformer acrobatics to achieve any sort of composition.



To unsubscribe from this group and stop receiving emails from it, send an email to friam+unsubscribe@googlegroups.com.
Reply all
Reply to author
Forward
0 new messages