no formal definition of "thenable"

[ikravets]

It seems like the spec uses the word "thenable" several times, but it's never formally defined. See for example

• 27.1.1.4 The AsyncIterator Interface
• 27.2.2.2 NewPromiseResolveThenableJob ( promiseToResolve, thenable, then )

I think it's better to provide an exact definition for "thenable".

[bakkot]

Ehhh, defining it precisely is tricky - what does it mean to "have a method", precisely, in a world with proxies?

[raulsebastianmihaila]

what does it mean to "have a method"

The spec defines a method as a function that is the value of a property of an object (with different words). Where is the challenge?

[michaelficarra]

@raulsebastianmihaila well then that term couldn't be used when defining "thenable", could it?

[raulsebastianmihaila]

Of course it can be used, what's the challenge?

[michaelficarra]

@raulsebastianmihaila again, it is proxies

[bathos]

@michaelficarra and even just accessors, or ordinary objects inheriting from proxies or objects with then accessors, etc. For that matter, “thenable module namespace exotic objects” or even “thenable sloppy mode arguments exotic objects”!).

The spec does have some pseudo-definitions with these same problems currently, i.e. attempts to provide “shape” definitions for things that are, at runtime, actually categories of programs, not categories of values. I think it probably shouldn’t (or that they should be moved into a non-normative glossary), but I don’t think this would be without precedent.

In runtime terms, the only sound definition of a “thenable value” is an object, nothing more. The runtime definition of interest occurs in the form of algorithmic steps from which the authorial-intention/non-runtime type-like-notion of “a thenable” emerges. Unbranded contracts produce the “feeling” that a category of values exists (e.g. ”iterables”) by design, but to soundly define the author-intent notion of “thenable value” (itself the product of a user-code-calling runtime algorithm) in runtime terms would be a definitionally impossible paradox even if it weren’t also trying to do so using (likewise undefinable) declarative language.

I don’t think that means there’s nowhere a definition of this sort could live or that adding it lacks value — just think it’s important to be clear that there’s no way a definition of this sort can describe the real set of interest which is like “application states wherein a given value would, if immediately asked to, sing a beautiful rendition of the then song.” For this reason I think adding any qualifiers aiming to make the definition already present in this PR “more true” would make it worse, not better: the starting point describes an author intuition plainly, at least, and that’s its value, while refinements diminish that value without actually making it more sound.

[raulsebastianmihaila]

again, it is proxies

You're very cryptic. What's the challenge with proxies?

The definition from #2869 is pretty close. A 'thenable' is an object that has a property (own or inherited, this extra wording doesn't need to be part of the definition) whose key is 'then' and whose value is a function. 'Has a property' here needs to be understood in terms of observing that the object has that property (and there are a few different ways to do that). It seems you're suggesting there's an issue with this definition because of the dynamic aspect of the JS language. I don't see any issue with that. JS is a dynamic and stateful language. An object (depending on its state) can be at one point a thenable and afterwards it can stop being a thenable. There are also some invariants and tools in the language to make things more predictable, such that a thenable object can continue to be forever a thenable. For instance, if the then property is an own data property, you can freeze the object. If it's an own data property of the obect's prototype, you can prevent extensions on the object and freeze the prototype object. There is of course also the case of the getter, in which case you can not know in advance, without knowing the algorithm in that getter, what the value of the property will be and that's fine. It is enough to observe at any point whether the object has that property and its value. Similar to the definition of the word 'method', as explained in #2846, things need to be understood in terms of relationships and not only in terms of what they consist of intrinsically. And to be maximally clear, the value can be observed using the [[Get]] operation (for instance by evaluating a property access), or using a [[GetOwnProperty]] operation and looking at either the value attribute or at the value of the 'get' attribute, if it's undefined, or at the result of calling the value of the get attribute, if it's a function.

[raulsebastianmihaila]

Actually, reading the definition from #2869 more carefully, I see it's good enough. Another way to express it would be: a thenable is an object that has a method whose key is 'then'.

[devsnek]

why do proxies complicate this? if they're well behaved then they either conform to the definition or they don't, like a normal object. if they aren't well behaved then it doesn't matter either way?

[bathos]

It seems [@michaelficarra is] suggesting there's an issue with this definition because of the dynamic aspect of the JS language. I don't see any issue with that. JS is a dynamic and stateful language.

That’s the zone where the meta-issue lives, yep.

An object (depending on its state) can be at one point a thenable and afterwards it can stop being a thenable.

From the POV of algorithmic steps effecting the illusion of that category existing, the category does not exist, so this isn’t true. Oops, getting sucked in, sorry —

The meta layering problem thingie can’t be reasoned away, but it already exists in the spec and I think this specific PR just drew a short straw by attracting discussion related to it. So long as there continue to be no references to the afflicted definitions in algorithmic steps or other specs, “technically unsound” gets pronounced with a hard technically. And since the value they provide is to document higher-level semantic intentions of contractual algorithms, whether big or small, they do their job regardless. If [Normative (Truthy Vibes)] mode is ever cleaned up it’d probably happen in a big editorial PR, not this one.

things need to be understood in terms of relationships

Definitions for ~higher-level semantic intentions of contractual algorithms~ 🤔 relationship patterns should definitely prefer to reference one another.

It is enough to observe at any point whether the object has that property and its value.

ahhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhh stop temptttting me nooooo this isn’t actually relevant but ^{evaluating the contract (a program) can call into user code. it cannot be skipped in these examples and it can always impact application state and it can always throw even if you previously established an invariant about the only possible normal completion value one of its OIMs can return and “sometimes invariant” rounds to “never invariant”}

[raulsebastianmihaila]

bathos's comment looks like word salad (and potentially trolling) to me.

[bathos]

@raulsebastianmihaila I can assure you there’s no trolling. I can offer no assurance about its quality, of course, and am sorry you found it lacking.

[zloirock]

I absolutely agree with @raulsebastianmihaila. Proxies do not change anything. If it's an object and on getting a .then property from this object, you get a callable object - it's a thenable - and here makes no sense is this a real property or not, and will this property be available after getting / calling or will it be removed after that - anyway, "thenable" is something about a duck typing.

If it walks like a duck and it quacks like a duck, then it must be a duck

[bathos]

If any folks have ended up tackling ghosts and/or windmills because my attempt at describing an existing formalization problem (only indirectly related to this PR) was unsuccessful, apologies. I think @bakkot / @michaelficarra were likely speaking about that same problem, and if so a distinct issue (with a description written by anyone but me lol) would probably prevent further confusion.

[michaelficarra]

If it's an object and on getting a .then property from this object, you get a callable object - it's a thenable

Right, so is that the wording you think we should use for the definition?

[zloirock]

Right, so is that the wording you think we should use for the definition?

The definition from #2869 LGTM. However, if it confuses you - it can be changed to something like what you quoted.