tail recursion modulo context

Stream: general

[Asei Inoue]

I have found this paper today: Tail recursion modulo context: An equational approach (extended version)

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/tail-recursion-modulo-context-an-equational-approach-extended-version/CCFFA4B8583A4924F002B0C377394303

That sounds nice

[Asei Inoue]

Should Lean have this...?

[Asei Inoue]

anyone else interesed in this?

[Markus Himmel]

You've linked to an 68-page PDF without any explanation about how it might be relevant to Lean or why people from this Zulip might be interested in it. If you want to get a discussion going, it would probably help if you summarized the ideas in the paper, how they apply to Lean, what problems they would solve that Lean currently has (ideally with examples), etc.

[Asei Inoue]

Thanks!! sorry

[Asei Inoue]

Here is abstract of this paper: (quoted)

The tail recursion modulo cons transformation can rewrite functions that are not quite tail-recursive into a tail-recursive form that can be executed efficiently. In this article, we generalize tail recursion modulo cons (TRMc) to modulo context (TRMC) and calculate a general TRMC algorithm from its specification. We can instantiate our general algorithm by providing an implementation of application and composition on abstract contexts and showing that our context laws hold. We provide some known instantiations of TRMC, namely modulo evaluation contexts (CPS), and associative operations, and further instantiations not so commonly associated with TRMC, such as defunctionalized evaluation contexts, monoids, semirings, exponents, and fields. We study the modulo cons instantiation in particular and prove that an instantiation using Minamide’s hole calculus is sound. We also calculate a second instantiation in terms of the Perceus heap semantics to precisely reason about the soundness of in-place update. While all previous approaches to TRMc fail in the presence of nonlinear control (e.g., induced by call/cc, shift/reset, or algebraic effect handlers), we can elegantly extend the heap semantics to a hybrid approach which dynamically adapts to nonlinear control flow. We have a full implementation of hybrid TRMc in the Koka language, and our benchmark shows the TRMc transformed functions are always as fast or faster than using manual alternatives.

[Asei Inoue]

According to the claim of the paper, it suggests that “by improving the compiler, one can relax the conditions required to benefit from tail-recursion optimization.” The authors say they have implemented this in the Koka language, but it might be possible to implement it in Lean as well.

[Asei Inoue]

I often write programs in Lean, but rewriting functions to be tail-recursive is tedious, and making them tail-recursive often makes the code harder to understand. I had been hoping for a way to automatically transform functions into tail-recursive versions, but according to this paper, tail-recursion optimization could be extended to functions to which it traditionally could not be applied. I think this would be a welcome improvement for many users.

[Asei Inoue]

I think implementing this would require modifying the behavior of Lean’s compiler, but is that something a user could do without directly editing Lean’s source code? I’ve never tried changing that part myself, so I’m not sure.

[Henrik Böving]

Asei Inoue said:

I have found this paper today: Tail recursion modulo context: An equational approach (extended version)

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/tail-recursion-modulo-context-an-equational-approach-extended-version/CCFFA4B8583A4924F002B0C377394303

That sounds nice

I've read this paper before and I'm not convinced we want to have this, at least not as a default. What exactly Lean does to your code is already not quite as predictable as we'd like. If we suddenly start doing transformations that may or may not convert your code from tail recursive to non tail recursive people might end up being confused why minor changes to their previously perfectly looking code suddenly cause it to stack overflow, while this is currently very clear with the "ordinary" tail recursion optimization. The most useful application of this optimization I've seen so far is in OCaml where you basically tag your function with the [@tail_mod_cons] attribute. This attribute has two crucial effects as you can see from the docs:

1. You get a compiler notifcation if the optimization does not apply
2. You get a compiler notifcation if it is unclear how to apply the tmc optimization because there can be multiple ways to do so sometimes

So if we end up doing this at some point I'd much prefer having the OCaml flavour rather than the Koka approach of just do it when it's convenient.

[Asei Inoue]

@Henrik Böving Thank you!!

[Asei Inoue]

tail_mod_cons attribute looks great!

[Henrik Böving]

I think implementing this would require modifying the behavior of Lean’s compiler, but is that something a user could do without directly editing Lean’s source code? I’ve never tried changing that part myself, so I’m not sure.

Oh and regarding this, that is possible yes, the compiler has a hook called @[cpass] that lets you inject things from the outside just like many other components from Lean. I would say this part of the API is far from being stable though

[Asei Inoue]

Im glad to know cpass tag! Thank you very much

[Asei Inoue]

Lean will have API for editing compiler which is open to user?

[Henrik Böving]

@[cpass] does allow you to do that, though I would currently not rely on doing anything important with it

[Asei Inoue]

oh my question was bad…

Lean will have stable API for this?

[Henrik Böving]

I don't know whether we are going to declare the compiler stable. Certainly not in the near future

[Robin Arnez]

I guess a more powerful variant of @[csimp] would be reasonable but adding entirely new compiler passes that affect the IR as a whole seems hard to get stable (at least for now)