T(R)MC: only specialize explicitly-annotated calls

[gasche]

This PR (against 4.14) implements a restriction to the tail-modulo-cons specialization: we only specialize tail-modulo-cons calls that are explicitly annotated with the [@tailcall] attribute.

Before:

let[@tail_mod_cons] rec map f = function
| [] -> []
| x :: xs -> f x :: map f xs

After:

let[@tail_mod_cons] rec map f = function
| [] -> []
| x :: xs -> f x :: (map[@tailcall]) f xs

This restriction has been suggested by @gadmm, see #10740 (comment). Personally, I am rather in favor of the previous behavior, where non-ambiguous calls in TMC positions (there is only one callsite that could be optimized in this branch) are implicitly specialized. However, the reasoning is that it will be easy to relax the restriction in the future, should people agree that it is desirable, whereas it would be harder to impose it later once the feature is released.

Unfortunately, it may be too late in the 4.14 release lifecycle for this change. (cc @Octachron) Arguments in favor:

1. The implementation change is minimal and we had good testsuite coverage.
2. This feature is not currently used in the wild, at it was never released yet.

I have not updated the TMC manual yet.

With this change, we could in theory simplify away sizeable parts of the TMC codebase, that take care of producing good warnings based on whether the TMC specializations are implicit or explicit. (Now they are always explicit.) However this would make the diff much larger, risk introducing other issues, and it would make it difficult to revert to the previous behavior later. I would be in favor of waiting until (we are not in release-hurry and) we receive a first batch of feedback from TMC users.

[gasche]

Note: the change to the implementation is very simple, but the changes to the testsuite were tricky at times and requested some thinking. (In some cases I had to disable some tests completely.) To potential reviewers I would recommend reading those changes carefully, to ensure that we agree that the new behavior makes sense.

(A first iteration of this PR would also require explicit [@tailcall] annotations on calls that are directly in tail position, not in "tail modulo cons but not tail" position. This is not the expected behavior, and I realized it by updating the testsuite.)

[Octachron]

If our aim is to receive a first feedback from users, I have the the impression that it would also make sense to provide both implicit and explicit specializations (as it is done currently) and observe which option people naturally adopts.

And since we already have the inference machinery, if we decided to remove implicit specialization, we could use during the migration period to provide good migration hints. That sounds like a sensible compromise for an experimental and opt-in feature.

[gadmm]

Thanks for this PR. The idea is that the documentation has to explain all kinds of warnings currently, and the design has a chance to become much simpler on this point with mandatory annotations at call sites. Now it would be a breaking change to explore and evolve the design in this direction after 4.14 without something like this PR.

Now I actually had in mind a TRMC-specific annotation, e.g.:

let[@tail_mod_cons] rec map f = function
| [] -> []
| x :: xs -> f x :: (map[@tail_mod_cons]) f xs

but perhaps the difference is not important.

Motivation for this PR depends on how interesting is this direction. So let me ask a bit more about it.

To me the next natural evolution would be to omit the annotation on the let:

let rec map f = function
| [] -> []
| x :: xs -> f x :: (map[@tail_mod_cons]) f xs

(also works with [@tailcall] instead of [@tail_mod_cons] but I suspect one would prefer the more explicit one in a first time.)

• Is this realistic in general or am I missing something?
• With or without annotations on let, does it allow you, as I suspect, to cut through a lot of tedious explanations about warnings (in the docs, and thus, also in practice)?

[gasche]

Yes, I think that some of the "ambiguities" described in the documentation would go away, it could simplify several corner cases.

On the other hand, I am not in favor of removing the annotation at the definition site, because I think that it maps closely to the mental model where the whole function definition is transformed, this is not just a local transformation on the callsite.

[gadmm]

After a short technical discussion with Gabriel he convinced me that it is good in a first time to the make the following style mandatory:

let[@tail_mod_cons] rec map f = function
| [] -> []
| x :: xs -> f x :: (map[@tailcall]) f xs

as this PR proposes.

My personal opinion is that in many years, it might make sense to ask if the following is not natural, once people are comfortable with the feature:

let rec map f = function
| [] -> []
| x :: xs -> f x :: (map[@tailcall]) f xs

and thus change [@tail_mod_cons] to make the annotation on let optional. It is premature to discuss this opinion but this PR will leave the door open.

So I am in favour of this PR which opens the most doors for future evolution.

It would be useful to include in this PR the update to the documentation in order to judge the simplification (unless @Octachron has already decided against late inclusion in 4.14).

[Octachron]

Looking at the documentation, as far as I can see, the proposed change will only enable to remove a single paragraph in the documentation (the implicit example in the disambiguation section).
I don't see a future where we will remove the toplevel annotation: this is a whole function transformation.
Overall, the proposed restriction seems to optimize for the worst case scenario. Even if I kind of like its explicitness.

Anyway, I am not short-circuiting the review process to integrate a last-minute feature change one week after the first (private) release candidate.

This PR is out of scope for 4.14 .

If the implicit specialization is problematic, we will issue a breaking change (with both a migration and backward compatible fix) on this new experimental feature in later versions.

[gadmm]

I had to look at it for myself. §10.24.1 and §10.24.2 will disappear entirely because any remaining situation with confusing error messages are replaced with straightforward situations with self-explanatory error messages, which do not need dedicated documentation. This is already 40% of the doc page. In the rest, there are smaller simplifications, such as when having to explain the impact on evaluation order (you can say that the annotation on tail call changes the order of the call), and where it refers to two other situations where not having an explicit annotation on call sites is confusing.

The current documentation already shows that implicitness at call sites is problematic. Moreover, the complexity seems to stem from trying to make a mental model out of an implementation detail (that this is implemented as a whole function transformation with specialized implementation).

You are right that the feature is explicitly declared experimental in the documentation, which is enough wording to allow the possibility to break user's programs in the future. (Though it would have been nice to avoid such breaking changes, and to make it non-experimental soon, so I understand Gabriel's desire to see this in 4.14!)

Given that future breaking changes are explicitly provisioned, it is hard to argue on that line, and so it is good of you to stand against a last-minute inclusion even for a tiny change.

[gasche]

I haven't looked at it in detail, but I would also make the guess, as @gadmm, that the simplifications in various cases could be substantial. On the other hand, I'm happy to see @Octachron taking a stand on release management instead of being accommodating to everyone all the time, so I'll be sure to respect his decision. (It's actually a cool trick to do release candidates without letting people know, an improvement over my strategy or releasing at random times.)

[Octachron]

I am not sure, but I had the impression that many issues with implicit annotations
like

    Let ((f v, map_vars f def), map_vars f body)

appear with explicit but erroneous annotations

   Let ((f v, (map_vars[@tailcall]) f def), (map_vars[@tailcall]) f body)

?

I would gladly be proven wrong however.

[gasche]

I updated the manual. The section on ambiguities is gone. @gadmm wrote:

§10.24.1 (disambiguation) and §10.24.2 (out of tmc) will disappear entirely because any remaining situation with confusing error messages are replaced with straightforward situations with self-explanatory error messages, which do not need dedicated documentation

The "disambiguation" section is gone for the reasons predicted. On the other hand, "out of tmc" remains.

The restriction implemented in the present PR is that calls that are in tail-mod-cons position but not in tail-position must be explicitly annotated. Calls in tail position in TMC functions are expected to become tail-calls, even without annotations. The "out of tmc" problem remains -- this expectation is broken if the called function is not tmc-specializable.
(One could require even more explicit annotations, but I don't like the idea that @tail_mod_cons would switch users into an entirely different mode where all tail-calls must be annotated.)

In the rest, there are smaller simplifications, such as when having to explain the impact on evaluation order (you can say that the annotation on tail call changes the order of the call), and where it refers to two other situations where not having an explicit annotation on call sites is confusing.

This prediction also came out correct.

Note: reworking the manual allowed me to locate a small issue with the current implementation which results in one of the examples not working as expected. I have not fixed it yet.

[Octachron]

The warning message needs to be updated too, since it seems the potential ambiguity of the TMC-transformation is not described anywhere

this constructor application may be TMC-transformed
in several different ways. Only one of the arguments may become a TMC
call

Maybe

  Only one call can be made tail-recursive under this constructor.

?

[Octachron]

I would expect that the manual keeps an example of conflicting annotations: It seems reasonable to explain that only one argument of a constructor can be transformed into a tail-call?

[gadmm]

(One could require even more explicit annotations, but I don't like the idea that @tail_mod_cons would switch users into an entirely different mode where all tail-calls must be annotated.)

We disagree on this, but then please adapt the examples in the section "out of tmc" to show the surprising case (implicit proper tail call). Currently it seems that at least some of the errors shown have become self-explanatory.

[gasche]

Before I put more work into this, I need to understand if it's ever going to be merged. If it's not going to be merged in 4.14, do we expect to have a permissive implementaion in 4.14 and a stricter one in 5.0? To me it sounds like we are not going to use the stricter behavior in practice, and I could just close and save my time.

[Octachron]

I would rather expect the contrary? If there is one implementation that works on both OCaml 4 and 5 and another one that is restricted to OCaml 4, I would expect people to use the backward compatible variant.

[gadmm]

Another option is to document the restriction now, to justify a later fix (with proper time to test it).

[gasche]

The best argument in favor of making the TMC subsystem more restrictive right now is that it's easier to relax things after the fact than to make them stricter. With this reasoning I was willing to go with the proposed restriction in the first release of TMC. If it's not going to be in the first release, if we have to deal with breaking early-adopter code anyway, I would rather wait to know for sure (with more feedback from users) that we want the extra restriction, it doesn't make sense (to me) to implement it in 5.0 just because.

In other words: the cost of including this change in "a later release" is higher than for "the first release", and I don't believe myself that this higher cost is counter-balanced by enough benefits.

(I'm not trying to complain about not including the restriction in 4.14, I think it's an entirely reasonable decision.)

Closing.

[gadmm]

Then, perhaps it was premature to merge the TMC feature. Either the “experimental” disclaimer in the documentation has a meaning or it does not.

its interface may evolve, with user feedback, in the next few releases of the language.

The best argument is the way the explanation of this feature is simplified and the way evaluation order becomes explicitly marked. I do not know what else you want, and I think that you have unrealistic expectations about the user feedback you can hope to get and the form that it would take. I was cautious to submit my feedback with verifiable arguments (I did not say, for instance, “reading the documentation makes me feel the design is backwards for no reason”, even if I find that there is some truth to this statement). So I do not care what you “believe”.

Given that you fell entitled to unilaterally close this PR with this argument, the conclusion for the future is: do not accept such “experimental” disclaimers as an excuse to merge admittedly unfinished designs!

[gasche]

Let's be clear:

1. On the whole, I rather agree that it would have been better to wait after 5.0 to merge TMC. Of course I was not aware of that when I proposed the merge, or when I merged. "hindsight is 20/20", as they say.
2. On the whole still (before I get into the details), I think that the details that we are discussing are, overall, no big deal: it seems that enough people are interested in TMC that having the feature available is better than not, and it's unclear that waiting more to debate fine points of the interface would make such a large difference. (Still my perfectionist self agrees that waiting a bit more to get an even better first proposal.)
3. As I said before, the change I proposed in the present PR has more value for me in a first release than in later release. I like it for 4.14, and I don't like it for trunk. I'm not going to push for inclusion of a change that I don't like myself, so I closed my own PR.
4. This is not related to the fact that this feature is experimental. We may propose breaking changes in the future if we see the need, but even for experimental features we need to be convinced that the value of the changes we propose offset their costs.
5. Your wording (I "feel entitled" to "unilaterally" ...) is insulting, please don't. What I'm doing here is protecting my time as a contributor -- yes, I can "unilaterally" close my own PRs!

[Octachron]

Given that you fell entitled to unilaterally close this PR with this argument, the conclusion for the future is: do not accept such “experimental” disclaimers as an excuse to merge admittedly unfinished designs!

@gadmm : don't forget that you are perfectly free to champion this change yourself and resubmit an equivalent PR with your own arguments and your own time on the line.