ponyc icon indicating copy to clipboard operation
ponyc copied to clipboard

Make ephemerality part of the capability, not the type.

Open plietar opened this issue 8 years ago • 2 comments

Today, the type A iso^ is represented internally by roughly TK_NOMINAL(A, TK_ISO, TK_EPHEMERAL). Because the ephemerality is distinct from the capability, it is easy to overlook it, even though it can have a lot of importance. This representation also allows meaningless types such as TK_BOX/TK_EPHEMERAL .

What I suggest is make A iso^ represented by TK_NOMINAL(A, TK_ISO_EPH). I think this matches better what ephemerality does. Ephemeral caps should be treated as completely different caps, such as in #1931.

The issue is this does not allow representing the types before the names pass, such as X^ or X!. We could keep the capability modifier (hat/TK_EPHEMERAL and bang/TK_ALIAS), and transform. I'm not sure whether the bang should exist at all after flattening and typeparam_set_cap is applied. It seems like it does exist today, I'm not really sure why.

This is a fairly significant change, so maybe it should just wait for the Pony rewrite of the compiler.

plietar avatar May 31 '17 23:05 plietar

@plietar this was discussed at the end of the sync. i think it would be good if you had a listen. i'll drop the link in here later when i upload it. i'm leaving this marked as "needs discussion during sync" for discussion on the next time you are on the call.

Sync audio: https://pony.groups.io/g/dev/files/Pony%20Sync/June%207,%202017

SeanTAllen avatar Jun 07 '17 20:06 SeanTAllen

Thanks for bringing that up on the sync. I see I wasn't really clear on the motivations for this change, so I'll try and explain in more detail.


Before getting into the details, I want to point to George Steed's thesis from last year. There's also a VUG somewhere I think. That's 144 pages, so I obviously wouldn't assume anyone to be aware of it, but many ideas I talk about here come from his work. For the curious I'll try to point to the relevant section of the thesis. Note that in the thesis, hat is - and bang is +. ie removes or adds an alias.

The compiler follows quite closely the model presented by @sylvanc in "Deny Capabilities for Safe, Fast Actors". George calls this model PonyS, and his "Comparison to PonyS" sections are quite interesting.


The way I'm coming with this is that in many places in the compiler, iso^ and iso are currently treated identically, ignoring the ephemerality. However, I believe in many (most?) cases, these should actually behave differently.

Here are a few examples :

  • It is safe to write anything to an iso^, but it isn't safe to write a ref to an iso (section 3.8). However, the cap_safetowrite function ignores ephemerality.

  • Viewpoint adaptation with an iso^ viewpoint is different from with an iso one. iso^->box is val, where as iso->box is tag (section 3.11.2, see caveat at the end). Yet the compiler treats both identically, eg https://is.gd/2mS189 doesn't build, but could/should.

  • iso is part of #any, but iso^ should not. Treating the two caps identically is (one of) the reason behind #1931

  • iso^ is a subtype of box, but iso is not (section 3.10). George Steed's definition and use of subtyping is quite different, and I'm not suggesting we change the compiler to match it (yet 😉 ). However, if we had this model of subtyping it could be difference between iso^ and iso.

My argument here is that iso^ and iso are fundamentally different capabilities, which "happen" to share the same prefix. They should therefore be treated as two different capabilities in the compiler.


On the call @sylvanc mentioned replacing gencaps by sets. This is pretty much orthogonal to this.

Also something about box^ being meaningful in the presence of generics. I didn't really understand this.


Caveat about viewpoint adaptation: it is important to point out that George split viewpoint adaptation into two different operators, extracting and non-extracting, which allows them to be more flexible than the current unique one. However even with the unique operator as implemented I believe the example of iso^->box vs iso->box holds.

plietar avatar Jun 08 '17 11:06 plietar