abstract operations don't always return Completion Records

[jmdyck]

5.2 "Algorithm Conventions" says:

Calls to abstract operations return Completion Records.

This is not always true.

For instance, consider GetFunctionRealm: when it doesn't return an abrupt completion, it returns a Realm Record. This is not a Completion Record, nor can it be implicitly converted into one (see 6.2.2.2), because a Realm Record isn't an ECMAScript language value, and so can't be the [[Value]] of a Completion Record.

Other examples:

• CreateListFromArrayLike returns a List.
• NewDeclarativeEnvironment returns a Lexical Environment.
• PrepareForOrdinaryCall returns an Execution Context.

[domenic]

It seems like this is split between two cases:

1. Cases where the abstract operation could conceivably throw, so some kind of "completion record that can contain spec types" would be useful. E.g. CreateListFromArrayLike already has a number of ?s in it that could propagate exceptions, so it's presumably already returning some kind of completion record for a List (despite that supposedly being impossible).
2. Cases where we're intentionally operating on high-level things (like execution contexts or environment records), away from ES values and potential throws, but still using the abstract operation formalism. NewDeclarativeEnvironment and maybe PrepareForOrdinaryCall fall into this category.

Very interesting.

[domenic]

It seems like this is split between two cases:

1. Cases where the abstract operation could conceivably throw, so some kind of "completion record that can contain spec types" would be useful. E.g. CreateListFromArrayLike already has a number of ?s in it that could propagate exceptions, so it's presumably already returning some kind of completion record for a List (despite that supposedly being impossible).
2. Cases where we're intentionally operating on high-level things (like execution contexts or environment records), away from ES values and potential throws, but still using the abstract operation formalism. NewDeclarativeEnvironment and maybe PrepareForOrdinaryCall fall into this category.

Very interesting.

[jmdyck]

E.g. CreateListFromArrayLike already has a number of ?s in it that could propagate exceptions, so it's presumably already returning some kind of completion record for a List (despite that supposedly being impossible).

Well, that's one possible way to resolve the inconsistency. (I.e., to say that "Calls to abstract operations return Completion Records." is always true, but the description of Completion Records is incorrect/incomplete.)

But to me, it seems like less of a stretch to say that the description of Completion Records is okay, but abstract operations don't always return Completion Records. Consider the sentence in 6.2.2.2 (which dates back to ES6 wd rev 6):

Unless it is otherwise obvious from the context, an algorithm statement that returns a value that is not a Completion Record, such as Return "Infinity" means the same thing as Return NormalCompletion("Infinity").

Without that "unless" clause, it would mean that every algorithm returns a Completion Record, either explicitly or implicitly. But the presence of the "unless" clause implies (and certainly allows) that sometimes, an algorithm can return something else. (And my guess would be that appearing to return a List, Realm Record, Lexical Env, etc qualifies as "otherwise obvious from context", though that's not essential to the point.)

[jmdyck]

E.g. CreateListFromArrayLike already has a number of ?s in it that could propagate exceptions, so it's presumably already returning some kind of completion record for a List (despite that supposedly being impossible).

Well, that's one possible way to resolve the inconsistency. (I.e., to say that "Calls to abstract operations return Completion Records." is always true, but the description of Completion Records is incorrect/incomplete.)

But to me, it seems like less of a stretch to say that the description of Completion Records is okay, but abstract operations don't always return Completion Records. Consider the sentence in 6.2.2.2 (which dates back to ES6 wd rev 6):

Unless it is otherwise obvious from the context, an algorithm statement that returns a value that is not a Completion Record, such as Return "Infinity" means the same thing as Return NormalCompletion("Infinity").

Without that "unless" clause, it would mean that every algorithm returns a Completion Record, either explicitly or implicitly. But the presence of the "unless" clause implies (and certainly allows) that sometimes, an algorithm can return something else. (And my guess would be that appearing to return a List, Realm Record, Lexical Env, etc qualifies as "otherwise obvious from context", though that's not essential to the point.)

[domenic]

After thinking on this, it seems much better to just have all algorithms return completion records. Saying that an algorithms ability to propagate exceptions should be coupled to whether or not it returns a JS value is bad.

[domenic]

After thinking on this, it seems much better to just have all algorithms return completion records. Saying that an algorithms ability to propagate exceptions should be coupled to whether or not it returns a JS value is bad.

[jmdyck]

Saying that an algorithms ability to propagate exceptions should be coupled to whether or not it returns a JS value is bad.

I agree, based on the examples of GetFunctionRealm() and CreateListFromArrayLike().

So, given that Completion Record provides the only way to propagate an exception, one solution is (as you suggest) to generalize Completion Record so that [[Value]] can be any value (spec value or language value).

But another solution is to decouple the "propagate an exception" possibility from the "return a value" possibility. That is, instead of representing those possibilities as instances of a single type of structure (CompletionRecord), we could put them into distinct value spaces (e.g., "abrupt completions" vs "normal values"), where "normal values" is the union of spec values and language values. (This decoupling is what I suggested in issue #497, for different reasons.)

The two solutions are presumably equivalent in expressive power, but I prefer the latter, mostly for reasons given in issue #497.

[jmdyck]

Saying that an algorithms ability to propagate exceptions should be coupled to whether or not it returns a JS value is bad.

I agree, based on the examples of GetFunctionRealm() and CreateListFromArrayLike().

So, given that Completion Record provides the only way to propagate an exception, one solution is (as you suggest) to generalize Completion Record so that [[Value]] can be any value (spec value or language value).

But another solution is to decouple the "propagate an exception" possibility from the "return a value" possibility. That is, instead of representing those possibilities as instances of a single type of structure (CompletionRecord), we could put them into distinct value spaces (e.g., "abrupt completions" vs "normal values"), where "normal values" is the union of spec values and language values. (This decoupling is what I suggested in issue #497, for different reasons.)

The two solutions are presumably equivalent in expressive power, but I prefer the latter, mostly for reasons given in issue #497.

[IgnoredAmbience]

Another location in the specification where this occurs is Evaluation of Property Access, where an exception can be thrown, but the Reference Specification type is returned.

In the JSCert ES5 formalisation, we compromised and treated References as an acceptable value in Completion Records, and had assertions/type checking in place to prevent them being unpacked into places where language values could only be accepted.
However, we also had implemented the union type method of abrupt completions and normal values for spec functions that returned pure values (ES5 had no implicit completion values) and had the opportunity to throw. We've only just realised we had used both approaches, and will move to the second approach in our current formalisation efforts.

[IgnoredAmbience]

Another location in the specification where this occurs is Evaluation of Property Access, where an exception can be thrown, but the Reference Specification type is returned.

In the JSCert ES5 formalisation, we compromised and treated References as an acceptable value in Completion Records, and had assertions/type checking in place to prevent them being unpacked into places where language values could only be accepted.
However, we also had implemented the union type method of abrupt completions and normal values for spec functions that returned pure values (ES5 had no implicit completion values) and had the opportunity to throw. We've only just realised we had used both approaches, and will move to the second approach in our current formalisation efforts.