search

jscert / jsexplain

Apache License 2.0
26 stars 4 forks source link

Spec is Inconsistent with Values in Completion Records #6

Open IgnoredAmbience opened 7 years ago

IgnoredAmbience commented 7 years ago

Completion record defined as only containing language values, however in a number of places specification values are returned (References, primary example).

ecma262 has a couple of interesting issues open on this topic, where we could potentially help: https://github.com/tc39/ecma262/issues/496 https://github.com/tc39/ecma262/issues/497

There's also work to add type signatures to the spec here: https://github.com/tc39/ecma262/pull/545

IgnoredAmbience commented 7 years ago

As noted in that thread the phrasing "Unless it is otherwise obvious from the context" phrase in section 6.2.2.2 is the trapdoor which allows for union return value types of Completion Records or Specification Values. Although it's hardly "obvious"!

IgnoredAmbience commented 7 years ago

See also tabatkins/bikeshed#673

IgnoredAmbience commented 7 years ago

GADTs a suitable means of typing throwing/non-throwing Completion Records for type inference of specification methods?

charguer commented 7 years ago

Hi Thomas,

I'm not sure to fully appreciate your question. Are you asking whether it is a good idea to involve GADTs for the typechecking of the Ocaml code describing the JS spec?

+ Arthur

GADTs a suitable means of typing throwing/non-throwing Completion Records for type inference of specification methods?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/jscert/jsexplain/issues/6#issuecomment-300808689, or mute the thread https://github.com/notifications/unsubscribe-auth/ABvu_LwZUYrg78BgShGLEyrQ9R6V7NIzks5r4xycgaJpZM4K2nxN.

IgnoredAmbience commented 7 years ago

Currently meeting with @johanneskloos, briefly discussing the project.

One aim I mentioned that the committee would like would be type inference for whether particular operations can potentially return abrupt completion records. As far as I can tell, the existing types we use cannot infer this at present. Requires further thought.

ByteEater-pl commented 2 years ago

Completion record defined as only containing language values, however in a number of places specification values are returned (References, primary example).

References used to be language values (albeit ECMA-262 didn't use this capability and user code couldn't return any either, so it was provided only for callable hosts objects (e.g. methods on hosts objects), and the only use I know of is E4X (ECMA-357)), ES5 changed that.