Formal Viewpoint Adaptation (George Steed's model)

[jemc]

Rendered.

[SeanTAllen]

I'm very excited to see this happen!

[SeanTAllen]

Small thing to add to the RFC. Sylvan and I would like this see this implemented where we:

• Do a release before the implementation of this is merged
• Merge the implementation of this
• Release this on its own

[shelby3]

I think George Steed might have an error in wording or a typo in his paper, and I can’t find an email address for him, so I will place my comments here. Hopefully one of you can forward to him if I have raised is a valid issue.

I quote from §2.2.1 Pony Capabilities:

as well as allowing modifiers to denote the property that a value is unaliased by adding a caret after the capability, such as Baz tagˆ

But the tutorial section Ephemeral types says:

That is, it's a type for a value that currently has no name (it might have a name through some other alias, but not the one we just consumed or destructively read).

The tutorial says the ephemerally referenced value is not always unaliased. Only the consumed (or destructively read) named reference loses its alias which is transferred to the ephemeral reference. I understand that the ephemeral reference is unnamed until it is assigned to a name, but non-exclusive reference capability types may have aliases other than the ephemeral reference.

Perhaps George intended to write ‘reference’ instead of ‘value’? So maybe it’s just a typo and not an error in conceptualization? Although wouldn’t the correct way to write that be, “…as well as allowing modifiers to denote the property that a reference is an unnamed alias by…” I have not completely read the paper yet, so I don’t know if I am incorrect for raising this issue or if that is just a typo or [very unlikely] if it is a conceptual error that carries through the paper.

EDIT: perhaps George meant “mutably unaliased” because I read in §3.3.1 Ephemeral Modifiers that he is only interested in ephemeral modifiers on iso and trn?

---

In §2.2.2 Viewpoint Adaptation the “and ω to refer to an object” doesn’t agree with Figures 1 and 2, which instead are labeled with ι.

---

Another typo in §2.4 F-Bounded Polymorphism:

[…] it is impossible to return any class more specialised that Cloneable.

I believe he meant “than” but that would still be misleading. As it would seem to imply that Cloneable is the returned class, but it’s Object. So better to write “than the return type in”.

---

Another typo in §2.6.4 Modelling Challenges:

[…] which allows expressions [with] potentially dangerous combinations of capabilities to be constructed.

Missing ‘with’ as shown.

---

Another typo in §3.4.3 Compatibility with Ephemeral Capabilities and Types:

Now that we have a definition of what[which] capabilities can co-exist with one-another […]

Incorrect word ‘what’ as shown.

---

Another typo in §3.11 Viewpoint Adaptation:

It is for this reason we now proceed [to] define viewpoint adaptation […]

Missing ‘to’ as shown.

---

Another typo in §3.11.2 Non-Extracting Viewpoint Adaptation:

Non-extracting viewpoint adaptation expresses the capability at which an actor α may see through an object ι to a field [object] ι' […]

Missing ‘object’ as shown.

---

I’m wondering why in §7.6 Recovery to correct a bug in Pony, he chooses to not recover the capability for any of the elements of a tuple, when it seems to me that the programmer could identify one of the elements for which the capability could be safely recovered?