8 ms·
My brain has been slowly trained to reject imperative programming. This example could be rewritten in a tail recursive manner using an immutable set which would
by norir 1y ago
My brain has been slowly trained to reject imperative programming. This example could be rewritten in a tail recursive manner using an immutable set which would be simpler to verify for correctness even without a formal verifier.
I have found that while there is a learning curve to programming using only recursion for looping, code quality does go significantly up under this restriction.
Here is why I personally think tail recursion is better than looping: with tail recursion, you are forced to explicitly reenter the loop. Right off the bat, this makes it difficult to inadvertently write an infinite loop. The early exit problem is also eliminated because you just return instead of making a recursive call. Moreover, using recursion generally forces you to name the function that loops which gives more documentation than a generic for construct. A halfway decent compiler can also easily detect tail recursion and rewrite it as a loop (and inline if the recursive function is only used in one place) so there need not to be any runtime performance cost of tail recursion instead of looping.
Unfortunately many languages do not support tail call optimization or nested function definitions and also have excessively wordy function definition syntax which makes loops more convenient to write in those languages. This conditions one to think in loops rather than tail recursion. Personally I think Lean would be better if it didn't give in and support imperative code and instead helped users learn how to think recursively instead.
- kevindamm 1y agoWhich languages do support TCO at this point? From my recollection we have * Scheme * Haskell * Elixir * Erlang * OCaml * F# * Scala * (not Clojure) * the JVM could remove tail-recursive calls, but IIRC this still hasn't been added for security reasons * Racket * Zig * Lua * Common Lisp, under certain compilers/interpreters * Rust? (depends) * Swift? (sometimes)
- nhubbard 1y agoKotlin as well, through the ‘tailrec’ marker on a function.
- kevindamm 1y agoah, thanks, good to know.. but does that make it optional? I kind of like how ocaml requires a letrec annotation on any recursive definition and I don't know when you wouldn't want to add tailrec
- louthy 1y ago> * F# The .NET CLR supports the ‘.tail’ opcode which means that any .NET based language could support it. I’m hoping one day the C# team will get around to it. It seems like such low hanging fruit.
- alexisread 1y agoFreeforth (implicit) and Ableforth (deliberately explicit)
- taeric 1y agoI don't understand the security reasons on not removing tail calls. Any chance you have a good place to read up on that?
- kevindamm 1y agoIt was raised in one of the initial proposals, back in 2002 https://bugs.java.com/bugdatabase/view_bug?bug_id=4726340 https://bugs.java.com/bugdatabase/view_bug?bug_id=4726340 but that looks like a dead link and no wayback archive.. IIRC, basically it's because some parts of the JVM use stack unwinding to figure out what userland code is calling certain system code.. also the current stack frame has metadata about lock status used for allowing re-entrant locks that you lose if you elide the entire recursive call (which the initial proposal did by only removing the few bytecode instructions that set up the callstack frame and return from it). A more informal proposal from ~2016 allows for soft tail calls and hard (annotated) tail calls, with some restrictions that evidently avoid issues with system calls and lock/reentry maintenance: https://web.archive.org/web/20161112163441/https://blogs.oracle.com/jrose/entry/tail_calls_in_the_vm https://web.archive.org/web/20161112163441/https://blogs.ora... And a video by one of the JVM architects at Oracle about adding TCO for Scala https://www.youtube.com/watch?v=2y5Pv4yN0b0&t=1h02m18s https://www.youtube.com/watch?v=2y5Pv4yN0b0&t=1h02m18s Also previously featured here on HN, a way to do it that avoids security concerns, by using goto instead of strictly deleting bytecode instructions: https://news.ycombinator.com/item?id=22945725 https://news.ycombinator.com/item?id=22945725
- zabzonk 1y agoC++, depending on compiler and other stuff.
- geoffhill 1y agoBoth Clang and GCC have musttail attributes than can force tail calls at specific return statements in C/C++.
- rudy6912 1y agoAlso Fennel, both implicitly and explicitly with `tail!`. Source: https://fennel-lang.org/reference#tail https://fennel-lang.org/reference#tail
- Quekid5 1y agoIt's worth noting that some (many?) languages[0] only support TCO as long as you're calling the function itself in tail position. The usual cases were you'll notice this when implementing state machines in "direct style" or when doing continuation-passing style for control flow. TCO is more general than that in some languages where any function call in tail position can be turned into a direct jump. This obviously requires either 1) runtime support in some form or 2) a non-trivial amount of program transformation during compilation. [0] Scala's @tailrec is one I'm 100% certain of.
- louthy 1y agoI agree, but also folds, traversals, list-comprehensions, and recursion-schemes work well and can be even more resistent to common bugs than regular recursion. Although it’s hard to fault the simple elegance of recursion!
- deleted 1y ago[deleted]
- taeric 1y agoThis feels overly strong? I've certainly messed up my fair share of recursive calls. I don't know why, but I have actually gotten a bit stronger on the imperative divide in recent years. To the point that I found writing, basically, a GOTO based implementation of an idea in lisp to be easier than trying to do it using either loops or recursion. Which, really surprised me. I /think/ a lot of the difference comes down to how localized the thinking is. If I'm able to shrink the impact of what I want to do down to a few arguments, then recursion helps a ton. If I'm describing a constrained set of repetitive actions, loops. If I'm trying to hold things somewhat static as I perform different reduction and such, GOTO works. I think "functional" gets a bit of a massive boost by advocates that a lot of functional is presented as declarative. But that doesn't have to be the case. Nor can that help you, if someone else hasn't done the actual implementation. We can get a long way with very mechanical transformations, in the form of compilation. But the thinking can still have some very imperative aspects.
- tuveson 1y ago> I've certainly messed up my fair share of recursive calls. It’s a common enough problem that the “why is my program crashing” website is basically named after it.
- teiferer 1y ago[dead]
- ngruhn 1y agoAnother case for recursion is that you have to think of the base case. With loops people pathologically forget to handle 0, [], [[]], "", etc.
- buzzin_ 1y agoI have found it that if you invest some time in learning how to write quality for loops, the quality indeed goes up. Also, when writing for loops, you have to explicitly think about your exit condition for the loop, and it is visible right there, at the top of the loop, making infinite loops almost impossible.
- tsimionescu 1y agoI think you're in a tiny minority if you think it's easier to read and understand algorithms written using recursive tail calls than imperative loops. Even outside of programming, take a look at most work being done in algorithm research - you'll see that most often algorithms are described in an imperative pseudo-code, and using a mix of loops and regular recursion (not tail recursion), with maybe some mapping and filtering constructs in addition. Tail recursion in particualr is the least human-friendly way to represent looping. It mixes input and output parameters of the function in any but the most trivial cases. It also forces the caller to figure out what is the base value for all of the output parameters (often requiring a separate function just to provide those to callers). And it basically takes an implementation detail and makes it a part of your function interface. Even in math, you typically define recursive functions like f(x) = 1 + f(x-1), not f(x, y) = f(x-1, y+1); g(x) = f(x, 0).
- immibis 1y agoComputers are imperative. With imperative programming you can get better performance than with pure functional. (Using pure functional to wrap an imperative core still counts as imperative) Maybe you don't care about performance; IMO squeezing performance is one of the important applications for formal verification, as you can prove your fast insane algorithm is correct, whereas the slow obvious one is obviously correct. If your main concern is clarity, some things are clearer when written imperatively and some when written functionally.