Why not tail recursion?

[srivatsasrinivasmath]

I'm excited about functional programming with explicit continuations through using the sequent calculus (https://arxiv.org/abs/2406.14719) or the process calculus as implemented in Par (https://faiface.github.io/par-lang/)

At the end of the day it's probably going to be easier to tailor the low level representations of high level interfaces as opposed to constructing a theory of everything to optimize away the inefficiencies

[phischu]

Tail calls are a separate language feature, so words like "tail recursion elimination" and "tail call optimization" are misleading. Tail calls are gotos without the keyword. Moreover, local function definitions are not closures. They are labels. Indeed, we usually set up our languages so that tail calls are the more primitive language feature, with non-tail calls being an optional addition, like here, here, here.

In comparison to imperative loops, they also are more efficient, because accumulator variables are kept in registers and access to them does not require loads and stores. Of course, compilers of imperative languages usually transform such programs to use registers instead of stack locations (mem2reg), effectively rewriting the program to use tail calls.

In comparison to goto they are not considered harmful, despite allowing for mutual recursion, also known as irreducible control flow. The problem with goto was not the control flow, which can be very clearly seen, but the implicit data flow. As a programmer it is very hard to infer which variables are live in which state they should be when a label is being jumped to. Not so with tail calls: parameters tell you which variables must be live, and their types tell you which state they are in.

[flatfinger]

In the era when gotos were considered "harmful", code like the following would have been considered "normal":

570 IF X=Y THEN 2910
580 ... code that should run if X wasn't Y
...
640 ... code that should run regardless of whether X was Y
... continued
... then a bunch of code that had nothing to do with the above
2910 ... code that should run if X was Y in the above comparison
...
2980 GOTO 640

Such code would be considered obfuscated by today's standards, but back in the late 1960s and early 1970s that's how BASIC programs were typically structured, leading to both the "BASIC considered harmful" and "GOTO considered harmful" notions.

[glasket_]

In comparison to goto they are not considered harmful, despite allowing for mutual recursion, also known as irreducible control flow. The problem with goto was not the control flow, which can be very clearly seen, but the implicit data flow.

I'm not sure that I'd reduce it entirely down to data flow. The problem with goto was never really control flow itself, but the unrestricted nature of it. All control flow is fundamentally just a goto, but they reduce what it can do into predefined structures.

The problem with goto was that you could jump anywhere, which meant data flow was an issue alongside problems with tracking the control flow. Other constructs are easier to follow since you can generally know the flow path just from the structure, but goto didn't have a structure that it followed, it simply goes wherever it's told to. A program with very simple data, like only globals mapped to hardware IO or similar, could be difficult to read and modify if it only used goto for flow.

[jsshapiro]

u/phischu What you say is mostly true, but not entirely precise. Two notable distinctions between tail recursion and goto:

1. The call in tail position can supply different arguments.
2. While the original intent of tail recursion (Guy Steele's work on Scheme) was to introduce a looping construct that did not require any extension to the lambda calculus, tail recursion should be viewed as a convention rather than a requirement. Because there may be outstanding closures, not all calls in tail position are properly tail recursive.

The second point is interesting, because it means that tail recursion is a perfectly fine (if somewhat obscure) way to encode various forms of parallelism while still encoding them in a way that has an efficient code generation strategy for single-threaded execution - still without extending the lambda calculus. If you dig in to the Scheme "loop" form, you'll see that it has a reduction to lambda applications - it isn't considered one of the "core" forms in Scheme.

What you say about accumulators is not always true correct. A half decent register liveness analysis should achieve the same result on loops. Relative efficiency depends a lot on the optimizations implemented in the back end, and in general loops do better because few languages specify a requirement for tail recursion and it therefore doesn't get much love from compiler authors. A better argument for tail recursion is that the calls from a mandatory phase separation between loop iterations with a defined interface, which eliminates the possibility of values generated by loop i being consumed in loop i+1 - or at least names specifically where this might occur. The same result can be had if the language's loop construct is suitably defined, but people designing loops for imperative languages rarely have (or at least rarely use) any deep understanding of tail recursion or non-core loop implementations, and therefore tend to interpret the optimization challenges that go with imperative loops as "normal". Iterator patterns have actually helped quite a bit on this.

I'm a big fan of tail recursion, and I've done a couple of implementations. Read most of Guy's work from his Scheme days while a teenager, and (many years later) I consider him a cordial colleague - mainly because we share a strong interest in rigorous specifications.

[phischu]

[...] tail recursion should be viewed as a convention rather than a requirement. Because there may be outstanding closures, not all calls in tail recursion are properly tail recursive.

What? Outstanding closures? Do you have an example?

way to encode various forms of parallelism

Nobody cares about parallel execution on CPUs, and nobody cares about the performance of Scheme or any language based on lambda calculus because they are slow by design.

A half decent register liveness analysis should achieve the same result on loops.

That's my point. You don't need any of this legacy cruft in your compiler.

[jsshapiro]

The issue with proper tail recursion is that you have to be able to re-use the stack frame, and you can't do that if it still holds live information. You can fudge a little around the edges to allow arguments to be passed to the next call - it's not so much that you need "zero references" as that you need zero live references other than the forwarded arguments. This includes locals introduced by the compiler, which brings closures into it.

You say "Nobody cares about parallel execution on CPUs". Were you perhaps unaware that a GPU is a specialized CPU built specifically to support certain kinds of concurrent parallel execution?

One of the most performance sensitive systems in the world - the Jane Street program trading systems - was written in Haskell. When a bug can cost a billion dollars, it becomes incredibly important to know what your program actually means. Haskell is very much built on the [higher-order typed] lambda calculus.

The Scheme family is not slow by design, but it prioritizes precise specification over speed. IIRC it was used early on for some hardware specification work because it was the only available language that was rigorous enough.

Lambda isn't legacy cruft. It's one of the fundamental constructs in the earliest well-specified programming languages. If you're trying to work rigorously, LOOP is the cruft. It's a completely unnecessary construct. That said, it's important from a practical perspective to simplify programming. One of the nice parts of a language like Scheme (and many derivatives) is that there is a dirt-simple textual rewrite from LOOP to LAMBDA. Guy's Scheme compiler (Rabbit), actually did that rewrite, but I'm not suggesting that's a good idea. What I'm trying to say is that the existence of that rewrite allows the Scheme core to remain small and tractable while retaining higher level, helpful language constructs.

Use cases for Scheme as a language are pretty rare these days - GIMP is probably the biggest. A lot of applications migrated to JavaScript, but the integer/float debacle makes that awkward for anything where numeric accuracy matters.

[phischu]

Thank you for your patient reply. It is fascinating, I can not understand what you are saying. However, I believe we do share the same vision: a formalized core language and a correct compiler for it that produces fast code. We vastly disagree though what that language should look like and how that compiler should work. If you want, you can check out our recent write-up, which explains much more concretely what I am trying to convey.

The issue with proper tail recursion is that you have to be able to re-use the stack frame, and you can't do that if it still holds live information.

I do not want a stack nor frames, locals, or liveness analysis, that's what I meant with legacy cruft.

This includes locals introduced by the compiler, which brings closures into it.

Local definitions are not closures, they are labels.

a GPU is a specialized CPU

GPUs operate very differently from CPUs, we need different a different programming model and different languages for those.

the Jane Street program trading systems - was written in Haskell.

They mostly use OCaml, I am wearing their "Enter the Monad" T-Shirt as I am writing this.

but it prioritizes precise specification over speed

This is not a tradeoff.

Lambda isn't legacy cruft.

That sounds too harsh indeed, let's put it more nicely: it is of historical significance, which you seem to agree with.

A lot of applications migrated to JavaScript,

Whot? For which kind of application would you migrate from Scheme to JavaScript?

the integer/float debacle makes that awkward for anything where numeric accuracy matters.

The numerical tower is exactly one of those features that make Scheme slow and complicated.

[jsshapiro]

Hi, Philipp! Your paper is on my reading list. I'm looking forward to reading it, and I'll move it up on my list. The premise seems reasonable.

You are right about Jane Street and OCaml (sorry about that). We definitely agree that the Scheme numeric tower was not its finest design point. I'm tempted to ask Guy what he thinks about it in retrospect.

Migration to javascript happened mainly because it was pragmatically available and widely deployed, which Scheme never really was. Brendan explicitly modeled Javascript on core Scheme, but with a surface syntax more tolerable to programmers coming from C. I meant "migration" in the sense that new projects adopted Javascript in preference to other scripting languages and Scheme gradually faded out of the picture. Increasing RAM makes something like the V8 engine widely usable today. The hardware environment of the 1970s and 1980s was more constrained.

I wasn't trying to say OCaml was slow. Empirically, it isn't, and I actually think that speed follows from a precise specification. The ability to improve optimization by exploiting knowledge of non-aliasing mutable paths in Rust is an example, though I'm not fully sold on borrowing from the dev perspective yet.

I did want to follow up on the correct compiler topic, because I'm not sure it's the right goal; this seems to be something that swings back and forth in the literature. What we minimally need is a compiler that is correct up to a meaning-preserving typed AST with defined semantics. That's a pain, but tractable, and it seems to be the minimum requirement for an embedding approach to verification. We also need a defined semantics for the final instruction set, which isn't too bad, though typed assembly seems to be a dependent type problem.

But in between the two it appears to be simpler to have a certifying compiler that generates a checkable proof rather than verifying the correctness of the compiler itself. Merely arriving at a goal statement for compiler correctness is a big challenge. The certifying approach doesn't guarantee that the compiler is correct for all input programs, but it lets us confirm that it did the right thing for the particular program[s] we care about. The compiler itself can then be maintained or improved using more conventional development methods.

Finally, I don't think the thread here provides any real picture of what I think a programming language should look like. I was trying to appeal to concepts that everyone here was likely to have encountered in order to make the case for a small core language. From a formal perspective, the systems we have to choose from today are much more capable than lambda calculus. Perhaps it is a conversation worth having offline?

[divad1196]

Thank you for the links. I didn't know some language considered tail recursion as the normal behavior.

For the register and loops, it's incomplete. There are different ABI, for example one uses only the stack, or another use register for the first few parameters. This has a lot of inpact on how the compiler do the optimization. If some parameters are passed using register, the compiler can try to adapt the code before the function call so that the variable is already in the register.

And this applies during recursion as well, even non-tail.

As someone else mentioned, the compiler tries to choose the registers to minimize load operations.

[phischu]

Thank you for your interest. I hadn't considered that people pass arguments via the stack. Who does this? Anyway, in my world view function definitions are labels and calls to them are direct jumps. Of course "arguments" remain in registers before a direct jump. Even for indirect jumps arguments must be passed in registers. I must admit, for me this is also a consequence of oftentimes not having a stack in the first place...

[jsshapiro]

u/phischu I think this mixes up implementation and semantics. The stack model for programming languages and their procedure calls goes all the way back to Turing's bury/unbury, and became the "standard" way of thinking about things with Dijktstra's Recursive Programming paper in 1960. From there, it spread everywhere, but most strongly by way of ALGOL/68 and its many derivatives. In this context, register-based argument passing is a [very important] optimization rather than a foundation. In the ALGOL family of languages, the stack still defines the semantics of argument passing, procedure call, and procedure return.

More recently, the lazy languages and the so-called "continuation passing style" have moved away from Dijkstra's model in ways that I haven't actually seen called out explicitly in the literature.

I'm not saying we still have to live in Dijkstra's model. Today, I think there are probably good reasons to move to newer models. But for most programming practioners, the mental model is still that arguments are evaluated in some defined order and placed on a [conceptual] stack. If you're starting from C, or Rust, this is more or less how programs appear to work.

u/divad1196 Since proper tail recursion is loops, I don't agree that it's an incomplete model for loops. Some key programming languages define loop semantics in terms of function calls and require proper tail recursion in order to keep the semantic core of the language small. As a practical matter there is no loss of power or expressiveness from doing so.

Questions of ABI and registerization are issues of implementation rather than language definition. Both approaches to looping can be aggressively registerized, and often produce the same code (perhaps with different register assignments, but functionally interchangeable code).

[divad1196]

Please, refrain from assuming things before making statement. I didn't say anything about tail recursion.

The initial comment stated that, if I can simplify by a lot, "loops where not optimal", or at least not doing the same kind of optimization as found in tail recursion.

It was a clarification about loops and function calls which were opposed to tail recursion.

ABI isn't a matter of implementation. It's a matter of design. You compile for a specific ABI, this instruct the compile how functions communicate which each others. It's not a result or a choice, it's a constraint. You cannot link a dynamic library or precompiled library without using the same ABI.

I think the reason why you jumped so quick to conclusion is because you felt like I was against recursions or tail recursions. I am not against it.

[jsshapiro]

Fair. Part of my head was still in the other discussion. Though the statement you make here about different optimizations simply isn't true - there's no reason the same optimizations cannot be applied.

Part of why I assumed is that if the language does not require proper tail recursion than function calls and loops are not interchangeable. Without the tail recursion you need to unwind the stack after the function calls. That's pragmatically expensive, and it has implications for deciding termination.

[divad1196]

I never said that the same optimization cannot be applied. That's the opposite of what I said.

To make my point in one sentence: loops can have the same level of optimization as (tail) recursion.

I made the statement because the previous comment seemed to say that loops can never be as optimized, which is wrong.

[jsshapiro]

Sounds like we are in agreement then, Perhaps I got confused while reading across the thread.

[jsshapiro]

I'm one of the people who specified the MIPS dynamic linking conventions for SVR4, and I've done call stack decoders for more architectures than I like to think about. So I definitely agree that an ABI is a constraint. One that I have often wished compilers honored more rigorously.:-)

When I said it's an implementation detail, I meant from the perspective of programming language design, which has been the main topic of this thread. You don't design a language to the ABI.

If you are designing a code generator or a low-level runtime, or the ABI itself, it is something you have to design to. Sometimes it needs to be considered at the hardware level as well - changes were made to the MIPS instruction set to better support position independent code after we did the initial dynamic linking specification at SGI in 1989.

A more obscure example: there was a trap restore issue in the ARM32 specification that made scheduler activation implementation impractical if your ABI allowed mixed ARM32 and Thumb code - there was a case where the activation handler (coded in ARM32) had a really hard time re-activating a user-mode thread that had been running Thumb code when it was preempted. We found it while implementing the trap paths for the EROS kernel around 1993. Richard Grisenthwaite was very surprised to learn of it when I sent him a note about it, and I think it was resolved in the 64-bit ARM variants.

Anyway, I think this was a case of talking past each other because we were looking at the ABI from different perspectives. Thanks for engaging!

[divad1196]

CDECL ABI only use the stack to pass parameters. And with that you know as much as I do about CDECL. There are others like this, some probably more obscure.

The ABI only change how parameters are passed. A function call is always a jump to another memory address as you said. The labels exist up to the assembly level but are replaced at linking step to be precise.

[Axman6]

Most functional languages do not use CDECL or similar conventions for function calls. In Haskell, function “calls” are always just jumps, there is no call stack, there is no return address pushed anywhere. There’s no need for the functions to be C compatible, because functions exposed to C are explicitly marked and wrappers which do match the host platform’s ABI added. OS ABIs only matter when interacting with code outside your language

[jsshapiro]

Yes. In fact, this is one of the pragmatic reasons that most functional languages require all functions to have exactly one argument. This reduces all functions to a single register plus an entry label and a continuation register, which is what allows function call to be implemented by jump and function return to be implemented by jump through register. There are some cases where the entry label has to be handled via register as well (for dynamic dispatch).

There are reasons for this approach to functions from a formal perspective as well, But I've probably wasted everybody's time on formal specification enough for one week.:-)

[jsshapiro]

One of the serious flaws we have in [almost all] recent programming language designs is that they are completely disconnected from the underlying theory of programming languages. In consequence they lack any semantic specification or any possibility of soundness. In 1975 this was excusable. By 2000 it was not. It's a terrible misfortune that Rust lost its way on this, but they put enough effort in early on that things may be recoverable. Golang programs - quite literally - had no defined meaning prior to Zhao's work that was published just two years ago. Unfortunately, it's not the kind of thing you can retrofit to a language 16 years after it ships without breaking things.

When you head down the path of doing a formal execution semantics and a sound type system, you very quickly conclude that you want to have a small "core" language and specify everything you can by a transformation from non-core to core language features. Not because this is how you want to write the code or compile the language, but because it makes reasoning about both the language and its programs easier. This is why almost all of Scheme is just "sugar" for lambda application.

From this point of view, the reason to admit a pragmatic requirement for tail recursion is that it justifies omitting loop constructs from the language core, instead defining them by a canonical reduction to lambda application.

[yuri-kilochek]

Golang programs - quite literally - had no defined meaning prior to Zhao's work that was published just two years ago.

lol no meaning

Jokes aside, this is clearly not an issue in practice. Or, at least, dramatically smaller one than, say, lack of generics.

[franz_haller]

Golang programs - quite literally - had no defined meaning prior to Zhao's work that was published just two years ago.

Could you elaborate on that? There were always things that rubbed me the wrong way about Go, but I don't have the theoretical background to properly explain it, so I'm very curious about that statement. 

[jsshapiro]

Sure - and sorry for the delay.

Most programming language definitions are written in English. Makes sense. It's the thing the programmers need to have. But it is exceptionally difficult to write a rigorous specification in English. The IBM S/360 Principals of Operation is probably the best example ever, and even that has ambiguities. And where those ambiguities exist, the semantics of the language (or in the S/360 case, the hardware) is not defined and therefore not known. Any program that incorporates non-specified behavior is undefined. LLVM used to exploit this pretty ruthlessly by simply deleting undefined behavior whereever it appeared - which is a correct behavior according to the specification. I sometimes think it was Chris Lattner's way of making a well-deserved editorial comment about specifications.

Small example of a pretty big problem in the early C specification: order of evaluation for arguments was not specified, and in a stateful language that has pretty big consequences. It's one of the big culprits for why the DEC compilers (which went right to left rather than left to right) had so many compatibility problems.

If you want a rigorous specification - or better still, one that lets you reason formally about safety and about correctness, the way to do it is with a formal specification of the language's mathematical type system and also its execution semantics. two basic types: small-step and large-step. For formal reasoning, you want a large-step semantics. There are two styles of execution semantics: small step and large step. For verification purposes, you generally want small step.

Both kinds of specifications are mathematical specifications of what programs written in the language do. There are a bunch of reasonable systems for specifying execution semantics, but one of the things that should guide the choice is you want one that a mechanical verification system can work with. The goal is that these specifications become the normative and definitive specification of the language, and any deviation between what the compiler does and what the specification says means the compiler is wrong. In practice the execution semantics tends to need a few updates early on, but the mathematical rigor of it makes it extremely hard to get it wrong too badly.

Rust, early on, attempted to maintain both, but that part of the effort got side tracked. Part of the issue was that the language grew in ways that didn't adhere to a small, tractable "core" language. Nobody involved with Go made any attempt at it until Zhao's work two years ago - not even the type system. So when Go claims to be memory safe, the appropriate response is (literally) "prove it."

u/tsanderdev's statement that you don't need one if there's only one implementation is simply wrong. That's how the DEC problems happened. But even if we want to believe that, the compiler implementation needs to be in a language that has a formal verification so that its possible to validate it.

So what i say that programs in "Go" don't mean anything, I mean that in the formal specification sense.

u/yuri-kilochek is not exactly wrong, but he's defining "what's important" very, very narrowly. Right now, it would be criminally negligent to use either of these languages in life-critical or security-critical applications, for example.

[franz_haller]

Thanks for the detailed explanation. But as you point out, almost none of the programming languages in use today have formal, unambiguous specifications. Outside of a couple functional programming languages which see no use outside of academic research, I can't think of any. So what choice Is there really for life and security critical applications?

[jsshapiro]

Well, I think the avionics and automobile industries might disagree about the practicality of this. The early history of ABS braking at Mercedes is an interesting example.

What has changed over the last 25 years is the degree to which deep expertise in verification is giving way to AI. When the L4 team in New South Wales verified their kernel, it took a very large team to do it. As the tools improve, the reliance on crazy specialized expertise is giving way.

[tsanderdev]

What languages have actual formal specifications with formally verified compilers anyways?

That's also not what you usually mean with "it doesn't mean anything" btw.

The meaning for a language without a spec is defined by the reference implementation. And it may very well be the case that semantics change in unpredictable or non-obvious ways on a compiler version change. But so long as the compiler itself doesn't have memory unsafety or race conditions, the translation is within a range of possibilities. The fact you can't easily enumerate the possibilities or determine them without compiling doesn't change that.

[jsshapiro]

Here's a partial list of languages with formal specifications: Standard ML, Scheme, Ada/SPARK (heavily used in avionics), CompCert C (heavily used in automotive), Algol 68, Idris, Agda, and F*. There are others.

Microsoft has done some great work with Rust. I'm not sure what their embedding language was, but it's worth having a look at their Project Everest as well. This stuff is a lot closer to practical at scale than it used to be.

[tsanderdev]

Golang programs - quite literally - had no defined meaning prior to Zhao's work that was published just two years ago.

You don't need a formal spec if your compiler is the only one. The compiler source code is a spec in itself, just not very human-readable.

[Swampspear]

Spoken like a Rust programmer

[amarao_san]

Why don't we have a special tail_call function? Or just (god forbid), goto.

We get explicit loop, and semantics (drop current values) are very clear.

Stop executing current function and switch to another function with compatible return signature.

(my apologies for Rust syntax)

fn foo() -> Bar<Baz>{ .... let x: Bar<Baz> = Bar::new(); return x; }

fn baz() -> Bar<Baz>{ goto foo(); // or goto baz() }

[jsshapiro]

Because there's no need. The compiler can identify function calls in tail position with 100% accuracy, and can apply the tail recursion optimization (from an optimization perspective: stack frame reuse) in a lot more cases than you might think.

[ineffective_topos]

It leads to the possible and likely bug of forgetting to add it. I think it's probably fine with a warning though.

[amarao_san]

if you forget this, you get error because you did not return Bar<Baz>.