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.