ponyc
ponyc copied to clipboard
ponylang
RFC 59: Formal Viewpoint Adaptation
Adopt George Steed's formal model for viewpoint adaptation, including a new syntax for distinguishing between extractive and non-extractive viewpoint types.
Issue https://github.com/ponylang/ponyc/issues/3571 demonstrates two type system exploits that violate capabilities. One of the two of them can't be properly solved until we resolve this ticket here and adopt the new viewpoint adaptation system that distinguishes extracting viewpoint adaptation.
I've added #3578 as another soundness issue which could likely only be solved by this change (as otherwise there would be negative impacts to subtyping elsewhere).
@bb010g thanks for linking. This isn't quite an implementation of that full theory. It changes the subtyping model but no changes have been made yet for viewpoint adaptation (and I'd like to discuss before doing so). It doesn't have any behavior changes besides the fix to return subtyping. Otherwise it's only an error message change
I have recently had some worries about the way generic caps are represented in ponyc that make me worry that we cannot support more than one type operator that modifies generic caps without losing track of the mappings of which input caps correspond to which output caps.
I think ponyc skates by right now on the fact that we only have one type operator (viewpoint adaptation) but I fear that having more than one type operator will cause the potential for subtle holes unless we completely change the way we deal with generic caps (and such changes may even imply new limitations added to the language).
I haven't come up with a concrete example yet of such a soundness hole, so at this time it's just a vague worry to look further into.
We should discuss this further @jasoncarr0, maybe in the next sync call where we're both present. Hopefully we can find a reasoning that can assuage my concerns.
Agreed with the concerns, and I'd like to talk about this as suggested.
Worth mentioning my experiences here on subtyping: https://github.com/ponylang/ponyc/pull/3643/commits/2086614ed36897c3a98e9b5324347cc06701cb9a reverting the changes I had made based on documentation, and https://github.com/ponylang/ponyc/pull/3643/commits/77f62a01b7a5032707bad6098f9b01f944eace3f correcting the documentation. The usage of subtyping (is_cap_sub_cap_bound) between generic constraints in ponyc is odd...