Sorting out completion records

[bakkot]

I would like to get completion records sorted out. My current plan is to

1. Change the [[Value]] slot of Completion Records to allow it to hold any type of value, not just ECMAScript language value (thus resolving abstract operations don't always return Completion Records #496 via the first of the two solutions discussed in this comment)
2. Remove the bit which asserts that all runtime semantics return a completion record
3. Label each abstract operation with the type it returns (in prose), so that non-completion-record-returning operations are not said to return completion records
4. Ensure all callers of an abstract operation consume the returned value properly: in particular, if the operation returns a completion record, it is explicitly treated as such, and if it does not, it is not
5. Remove the bit which allows implicit unwrapping of completion records

I'm going to prepare a PR which does this as soon as I have time.

[bakkot]

(cc @jmdyck, who I know has some interest in this topic)

[brabalan]

I am willing to help with this. Our work on JSRef and JSExplain are written in OCaml, so they are typed and we've had to deal with this issue.

Regarding point 4 ("Ensure all callers of an abstract operation consume the returned value properly"), do you consider that monadic operators (? and !) do the job, in the sense that they only make sense if they are given a completion record?

[ljharb]

Yes, i think so.

[bakkot]

@brabalan That'd be great! Do you happen to have a link to your standard library definitions, and/or a list of places where the inconsistent typing in ECMA-262 has required workarounds?

do you consider that monadic operators (? and !) do the job

Yup. Though I intend (as part of step 4) to change the parts of their current definitions which say "if argument is a Completion Record, set argument to argument.[[Value]]" to just "set argument to argument.[[Value]]".

[brabalan]

We define the type for completion records here https://gitlab.inria.fr/star-explain/jsexplain/blob/master/jsref/JsSyntax.ml#L619 (we already cheat because we allow references, we plan to change that). For "completion records" that contain other things, we use https://gitlab.inria.fr/star-explain/jsexplain/blob/master/jsref/JsSyntax.ml#L683.

In https://gitlab.inria.fr/star-explain/jsexplain/blob/master/jsref/JsInterpreter.ml, anything that is bound with a let%spec is a specification value (i.e., a completion record that does not contain a value), and anything built with a res_spec is also a specification value. For instance, https://gitlab.inria.fr/star-explain/jsexplain/blob/master/jsref/JsInterpreter.ml#L502 corresponds to https://tc39.es/ecma262/#sec-topropertydescriptor which returns a completion record with a property descriptor (used in step 13 of https://tc39.es/ecma262/#sec-proxy-object-internal-methods-and-internal-slots-getownproperty-p).

[devsnek]

You might also be able to glean some inconsistencies from usage of EnsureCompletion in engine262, which wraps a value in a normal completion if it isn't already a completion.

[jmdyck]

1. Change the [[Value]] slot of Completion Records to allow it to hold any type of value, not just ECMAScript language value

Maybe not quite any type of value: in particular, I suspect it would be confusing to allow a completion record in the [[Value]] field of a completion record.

4. Ensure all callers of an abstract operation consume the returned value properly: in particular, if the operation returns a completion record, it is explicitly treated as such, and if it does not, it is not

Pertinent to that, over in PR #1907, @syg said that, post-reform:

• ! Op() means "Op can have effects on evaluation control flow. For this particular callsite, the only effect it can have is a normal continuation, i.e. evaluate the next thing."

• ? Op() means "Op can have effects on evaluation control flow. For this particular callsite, abrupt values are propagated immediately."

• Op() means "Op cannot have effects on evaluation control flow."

Note that there's a 4th possibility: "Op can have effects on evaluation control flow. This particular callsite can return an abrupt completion, but it is not propagated immediately." (It's uncommon, but it certainly happens.) In such cases, you can't use ! or ?, and yet the lack of a prefix would make it look like the third form, without the prescribed meaning. So you might want to think about a third prefix to convey that possibility.

[bakkot]

I suspect it would be confusing to allow a completion record in the [[Value]] field of a completion record.

It would certainly be confusing to put one there, but I'm not sure it's worth explicitly prohibiting it rather than just not doing that. Might be; I'll wordsmith both and see which I prefer.

So you might want to think about a third prefix to convey that possibility.

To my mind the most important thing is that it does not immediately affect control flow, and there's no other implicit magic happening on its return value, so you can understand what's going on in the algorithm just be reading what it says.

[jmdyck]

It would certainly be confusing to put one there, but I'm not sure it's worth explicitly prohibiting it rather than just not doing that.

The thing is, if the spec simply doesn't do that, it isn't obvious to the reader that it doesn't (and won't ever). So I think it's worth saying.

To my mind the most important thing is that it does not immediately affect control flow, and there's no other implicit magic happening on its return value, so you can understand what's going on in the algorithm just be reading what it says.

Yeah, that's okay with me. But then be sure not to describe the meaning of Op() as @syg did.

[michaelficarra]

There's nothing wrong with describing it in the way @syg did. The call of the AO doesn't affect the control flow. It doesn't matter if the AO returns a completion record and then somewhere else that completion record is acted upon in a way that affects control flow. That's a first-class value like any other and it is not strange.

[jmdyck]

The call of the AO doesn't affect the control flow. It doesn't matter if the AO returns a completion record and then somewhere else that completion record is acted upon in a way that affects control flow. That's a first-class value like any other and it is not strange.

I'm fine with all of that.

But when syg said "Op can have effects on evaluation control flow", that's not talking about a particular callsite, that's talking about all possible calls to Op. That is, Op can, under some circumstances, return an abrupt completion. (It has to mean that, otherwise you can't make sense of his description for ! Op().) So then syg's "Op cannot have effects on evaluation control flow" presumably means that Op cannot, under any circumstances, return an abrupt completion. Which is not true of the 4th possibility I described, or (probably) the situation you described above. So the description in syg's third bullet does not apply.

[jmdyck]

I'm going to step away from @syg's quote, as I think the phrase "can affect control flow" may be muddying the waters. Instead, I gather that after the reform proposed by this issue, the following case analysis would hold:

CR = completion record
AC = abrupt completion
"expr value" = the value that would be bound to _X_ in `Let _X_ be ... Op().`
               (if execution gets that far)

1. The operation cannot, under any circumstances, return an AC.
   The operation's return value is always a non-CR.
   Invocations look like `Op()` (no prefix)
   The expr value is a non-CR.

2. The operation can, under some circumstances, return an AC.
   The operation's return value is always a CR.

   a. This particular invocation never returns an AC.
      Invocation looks like `! Op()`
      The expr value is a non-CR (the CR's [[Value]] field).

   b. This particular invocation sometimes returns an AC.

       i. When the invocation returns an AC, the caller immediately returns that AC.
          Invocation looks like `? Op()`
          The expr value is a non-CR (the CR's [[Value]] field).

      ii. When the invocation returns an AC, the caller doesn't immediately return that AC.
          Invocation looks like `Op()`
          The expr value is a CR.

Given this, my points boil down to:

• If you describe cases 1, 2.a, and 2.b.i, don't leave out 2.b.ii.
• In this analysis, case 2.b.ii is not the same as case 1.
  (Mind you, the calling step can certainly handle them the same way,
  e.g. by binding the operation's returned value (CR or non-CR) to an alias.)
• You might want a distinct prefix for case 2.b.ii (but if not, that's fine).

[michaelficarra]

You might want a distinct prefix for case 2.b.ii

No thanks. It's just another value at this point.

[bakkot]

You might want a distinct prefix for case 2.b.ii (but if not, that's fine).

Thinking some more about this, I'm inclined to do something like "1. Let foo be the Completion Record returned by Something()". We don't normally emphasize return types like this, but I think it's probably worth doing so in these unusual cases.

[michaelficarra]

Plans from the editor call:

1. In AOs, always explicitly create completion records. Remove the provision for implicit wrapping in normal completion.
2. In AOs, always explicitly unwrap normal completions records. Remove the provision for treating normal completions as their [[Value]].
3. Every AO either always returns a completion record or never returns a completion record.
4. For any AO that returns a completion record, place an assertion at its call site that the value produced is a completion record.
5. Add a boolean to the metadata that distinguishes between AOs that return completion records and those which do not. Possibly lint for correctness of this metadata.
6. Define "return" in built-in functions to wrap an ECMAScript value in normal completion and return.

[bakkot]

Note that it may prove to be too noisy to wrap up AO return values in NormalCompletion, so we might end up wanting to do something else.

[ljharb]

For 4, can the assertion be terse, like ? and !, rather than an entire prose step?

[bakkot]

We already have an AO which does exactly this assertion: Completion(arg) asserts that arg is a Completion Record and returns it.

I don't want to be much more terse than this given how rare it is for callers of Completion Record-returning AOs to need to handle the Completion Record explicitly rather than via ? or !.

[ljharb]

In that case, the AO call site could be wrapped in Completion(), and that would be a sufficient assertion?

[bakkot]

Yes.

[jmdyck]

So as far as my earlier case analysis is concerned, am I right in thinking that the only update is that in 2.b.ii, the invocation looks like Completion(Op()) ?

[bakkot]

Yup.

[jmdyck]

In AOs, always explicitly create completion records. Remove the provision for implicit wrapping in normal completion.
...
Note that it may prove to be too noisy to wrap up AO return values in NormalCompletion, so we might end up wanting to do something else.

One possibility would be to allow implicit wrapping in NormalCompletion() if an algorithm is clearly marked as returning a Completion Record. (So generalize point 6 from functions to other algorithms.)

Another possibility would be to do away with normal completions (as in #497), so that if an algorithm says (e.g.) Return *"foo"*, then it's actually returning that String value, no explicit or implicit wrapping needed. Note that this isn't as radical as it might sound. The spec could look almost identical to what you're envisioning. In particular, you can still have all the call-site 'markup' that you want (although case 2.b.ii would change from Completion(Op()) to something else that indicates "this could be a normal value or an abrupt completion").

[jmdyck]

Could we continue the above discussion?

[bakkot]

I am not in favor of the proposal to do away with NormalCompletion entirely. (This is mostly on aesthetic grounds - I really don't like untagged unions - but also because it makes it harder to clearly communicate to the reader when code is working with completions, because there's no obvious way to write the Completion() assertion: it's hard to have an assertion that a value might be a completion.)

Regarding implicit wrapping: I'm personally fine with it, but I think @michaelficarra expressed more reluctance. @michaelficarra thoughts?

[jmdyck]

I really don't like untagged unions

But the spec is full of untagged unions. I count roughly 170 parameters that accept values of multiple types, and about 230 algorithms that can return values of multiple types (not even counting abrupt returns). E.g., InitializeBoundName's _environment_ parameter accepts an Environment Record or *undefined*, and ParseText returns a Parse Node or a List of errors. There's no need to 'tag' such unions because we can simply ask if _environment_ is *undefined*, or if a parse result is a List of errors.

(From another point of view, all unions are tagged because all values are tagged.)

but also because it makes it harder to clearly communicate to the reader when code is working with completions, because there's no obvious way to write the Completion() assertion: it's hard to have an assertion that a value might be a completion.)

Completion() means "this is either a normal completion, or it's an abrupt completion".

In a world without normal completions, we could analogously have MightBeAbrupt() or CouldBeAnAbruptCompletion() or NormalOrAbrupt(), meaning "this is either a normal value, or it's an abrupt completion". That doesn't seem hard to me.

[bakkot]

But the spec is full of untagged unions. I count roughly 170 parameters that accept values of multiple types, and about 230 algorithms that can return values of multiple types

Eh... with relatively rare exceptions (particularly for null and undefined), the different kinds of value represent similar things. An abrupt completion represents a very different kind of thing from a regular value.

(From another point of view, all unions are tagged because all values are tagged.)

By "tagged union" I mean specifically that it is impossible to consume the value without unwrapping it, so it is totally unambiguous to a reader whether a given line has accidentally neglected to consider some case of the union or has intentionally done so. So no, most unions in the spec are not tagged.

Specifically, if we allowed the "normal" and "abrupt" cases to be untagged, then someone reading

1. Let x be SomeAO(arg).
2. Let y be x + 1.

can't tell if SomeAO happens not to return an abrupt completion in this case and the author of these lines is relying on that, or if the author has simply failed to consider the case where it returns an abrupt completion, or it never returns an abrupt completion.

We could be disciplined in following an editorial convention of always using ! or ? or CouldBeAnAbruptCompletion when invoking algorithms which sometimes return abrupt completions, but that's just explicitly unwrapping, and if the union is untagged then omitting one of those three things would not obviously (to a reader) be an error. I would prefer that we arrange things such neglecting to unwrap is obviously an error rather than just a failure to follow an editorial convention.

(Yes, there are other kinds of returned values in the spec which have the same problem. In most cases the unions are fairly bespoke, such that describing the wrapping and unwrapping would add a lot of mental overhead. This particular union is very common, so we can reasonably introduce shorthands to reduce that overhead, and you only have to learn what it means once and can then understand its use in many many places.)

MightBeAbrupt() or CouldBeAnAbruptCompletion() or NormalOrAbrupt(), meaning "this is either a normal value, or it's an abrupt completion"

Assertions should constrain the possible set of values. In the scheme you propose, every value is either a normal value or an abrupt completion. So there is nowhere you couldn't put such an assertion.

We could be disciplined in only using NormalOrAbrupt in places where there is in fact some way to actually end up with an abrupt completion. But again, I would prefer that we arrange things such that failure to keep to this discipline is obviously an error rather than merely a failure to follow an editorial convention.