About tail calls

[FrankHB]

The test named 'proper tail calls (tail call optimisation)' in https://github.com/kangax/compat-table/blob/gh-pages/data-es6.js#L20 is actually a bug because it is technically incorrect and misleading.

First, derived from issue 819, PTC (proper tail call) is NOT TCO (tail call optimization). ES 6 mandates no TCO (tail call optimization), but "(proper) tail position call", and also introduces "proper tail call" in its Introduction chapter. As mentioned, PTC or proper tail recursion differs significantly from TCO in ways of specification and implementation. The fact is being widely confused even in some Lisp communities. It is deserved to be clarified.

The more generalized meaning or the essence of PTC can be related to the hierarchy of asymptotic space complexity classes of activation records. This is formalized in paper [Clinger98] for typical Scheme dialects. Even ES is still lacking a formal semantic model in this style, it can follow the properties in the hierarchy. This is definitely not an optimization even in users' view.

On the contrary, TCO (with or without so called "merging") is one of the common implementation techniques for PTC. TCO is not a must to implement PTC, for example, when the source language (the language to implement the object language) has mandatory support of PTC, it can be used directly. The case is usually not true for ES implementations due to interops and some other historical reasons, but ES spec also does not assume its existence.

Side note: Actually PTC in ES 6 is a weaker form to common ones since it only mandates the "position" in pure syntactic (static) flavor, omitting some other context which cannot be reduced directly from the static syntax (e.g. evaluation of a function body in evaluation of a function call expression, which itself is not attribute to the "call" here). This is problem of the language spec, not a bug here.

The second should be obvious: successfully execution with deep function calls does not indicate "proper". ES do specify that the resources must be released or reused. Even it is not formally sufficient, the intent should be clear. This can be hardly detected as it is not guaranteed to be observable in the host environment, but it at least deserves an explicit note to indicate readers the limitations of the test cases in the page.

[ljharb]

It seems like the actionable request here is to rename the test from TCO to PTC (which i agree with, hence my comment that you linked to); as for the test itself, i don’t see how what the spec mandates isn’t verifiable.

If this isn’t a correct interpretation, can you elaborate on what actionable things you’re hoping for?

[chicoxyzzy]

I think we should rename "proper tail calls (tail call optimisation)" to "proper tail calls" and move it from "optimizations" section to some another section

[FrankHB]

I agree that renaming is a correct direction; however, further clarification would be also beneficial, to who has been confused a while.

As of the test cases... it is technically difficult to implement, if it is not absolutely unimplementable, to cover the spec. The current test cases are defective because they do not measure the resource usage in any way. But even they could do, it would be still insufficient. By definition, the "proper" in PTC means it can allow unbounded number of active tail calls; in practice, despite the untestable nature of "unbounded number", it means the calls frames can be nested with arbitrary depth until it eats up all memory available in the implementation. Exhausting memory is hardly an acceptable condition anyway. Theoretically, the only reliable way is to analyze the code of implementation to prove it does have the guarantee, but this is also not practicably verifiable by test cases. So likely we have to compromise the sufficiency to make it feasible, by leaving the cases as-is, with additional notices to inform users the cases are not free from false negative results.

[ljharb]

If it’s not possible to prove the implementation meets the spec, then is the spec really implementable at all?

[FrankHB]

@ljharb It can be formally proved and implemented, but extremely complicated and costly in most realistic cases.

Since code of most languages being used to implement the object language is not formally verifiable, the proof needs to work with a full implementation of the object language. Such a proof will first work for a formal model. (In fact, [Clinger98] did prove the properties of proper tail recursion and its stronger variants held for some formal dialects of the Scheme language.) Then, by codifying the operational semantics specified in the model, it is implemented and the desired properties are kept (although there can be bugs hidden in the language used to implement the object language).

Most language implementations do not work like this because:

1. Only quite a few "real" languages (like RnRS Scheme and SML) have been specified with formal models in their specs. Most other languages are even not designed with this in mind. A new formal model will require extra work of verification of the conformance between the model and normative-but-not-formal specification at the beginning and at each update of the language spec, which is ineffective. And reviewing the specs cannot be done automatically so it will need many man-hours.

2. Although reasoning about relatively "small" properties like PTC can be done manually, the model is usually quite large for a full realistic implementation. Proof-of-concept models are usually printed on papers for reference; they are not fit in engineering. For product-level projects (like this, with TCO in the RTL stage, though no PTC guarantees in the language spec), the formal specification can be develop separately with proof assistants. This is very expensive compared to usual informal ways (although this approach overcomes the lack of models in the language spec).

3. Extra work needs to be done on formalization of optimization. Naive one-to-one mapping from the model is usually ineffective.

However, I believe PTC can be carefully implemented without formal methods. Once all the tail contexts are known, an implementation can perform an operation when it meets each tail context to prevent the growth of activation records. (The operation effectively releases the resources no longer kept in the context; if it is not possible, the specification of tail contexts is buggy.) Nevertheless, frequent operations can be harmful to performance so perhaps many implementations are not so strictly conforming. For example, implementation with nondeterministic collectors (typical tracing GCs) can seldom miss the opportunity to release the memory (like this).

And anyway, verifying missing of PTC is relatively easy with tolerance of false negative results, as the current test cases.