A sketch for stable functions

[rossberg]

Other than preventing their removal and incompatible type changes, allowing functions to be stable (or shared, which is almost the same) poses two additional challenges:

1. The function must be identifiable across upgrades, which may involve fairly arbitrary code changes.
2. For closures, the environment must remain compatible across upgrades, which may pair new code with an old closure environment.

To deal with (1), we can impose two restrictions:

• Stable functions must be named.
• Stable functions can only occur in stable functions.

Together, these allow identifying any stable function by their "name path" relative to the enclosing actor, which cannot change with upgrades.

For (2), the following seems like a plausible strategy:

• Stable functions can only close over stable declarations.
• As above, stable declarations (including values) can only occur in stable functions.
• The closure environment of a stable function is not represented as a tuple of values, but more expensively, as a map from stable name path to value; that way their access is position-independent and not affected by the addition/removal of parts of the closure environment when upgrading the function.

Effectively, the closure environment is a record parameter, and the rules for upgrading it follow from that. E.g., because parameters are contravariant, we can only safely allow shrinking the environment during an upgrade, unless we solve the contravariant field addition problem, which seems to require defaults.

One issue with all this is how to represent these constraints in an IDL-style "stable interface" that we would like to use for checking upgrades. It seems that such an interface would need to be explicit about stable locals as well as about the closure environment of stable functions. Seems nasty.

[nomeata]

Together, these allow identifying any stable function by their "name path" relative to the enclosing actor

Is that true? What about shadowing of names inside stable functions.

actor a {
  stable foo1() {
    let fun1 = { stable foo2() { return 1} }
    let fun2 = { stable foo2() { return 2} }
  }
} 

How would the name path to the two foo2 differ?

(I am very doubtful that anything that makes stuff besides top-level named entities stable, but maybe I am too pessimistic.)

[rossberg]

Well, I said they can only occur in stable functions. That excludes nested blocks. :)
If that's too restrictive we may introduce (named) stable blocks (and object literals?), too.

I tend to agree that this is all questionable, but it seems where you would have to go if you wanted to embrace stability more completely. You're inevitably gonna buy into some of the complexity and cost of the "orthogonal" kind of stability we were discussing over the last months.

Two possible simplifications avoiding much of the closure stuff: only allow functions closed-up-to-toplevel to be stable (sugar for toplevel functions); and perhaps do something special for stable classes, where methods may close over stable object fields and parameters, but nothing else. The latter is a more ad-hoc version of the above, but I fear we'll get some pressure to allow stable objects eventually.

[nomeata]

Is there convincing prior art for this kind of stuff, or is this exploring a pretty new design space corner?

[rossberg]

I am not aware of anything similar, unfortunately, but I may simply not know about it. For that reason alone I'd prefer if we didn't have to go there. Merely brain-dumping it here for later reference.

[matthewhammer]

FWIW, this reminds me of the usual set up from Contextual Modal Type Theory, where we have a "box" connective that is modal, and has its own special context, and special context rules.

[matthewhammer]

FWIW, here's a paper I read recently that reminded me of these ideas (recently): https://arxiv.org/abs/1703.01288

[luc-blaeser]

#4789