With exclusively static dispatch I feel like it should be possible to unconditionally detect at least the presence of recursion at compile-time, but in the presence of dynamic dispatch (as in the article) I think it might be impossible for a compiler to guarantee that it can statically detect recursion. (I have no basis for these claims other than gut feeling.)
> With exclusively static dispatch I feel like it should be possible to unconditionally detect at least the presence of recursion at compile-time,
This is equivalent to solving the halting problem, and therefore impossible in the general case.
Tools can use heuristics to make a guess. Dynamic dispatching to mutually recursive functions is one example where those tools fail. But that also includes things like checking a conditional before calling a function. The tool can check unconditional infinite recursion, but it can't tell you for certain that a branch that may be infinite is always taken.
Whether or not the recursion ever successfully reaches the base case in order to terminate is certainly equivalent to the halting problem, and thus undecidable for Turing-complete languages.
However, I was making a much weaker claim, which is that if you have exclusively statically-dispatched function calls, it should be possible for a compiler to detect the possibility of recursion 100% of the time.
For every function, you should be able to make a complete list of every other function that it calls directly (including branches that may never actually be taken at runtime (which it cannot know, because of the halting problem), making this overly conservative, like any type system). This list is both perfectly precise (because of static dispatch) and finite. With this, you can then construct a graph and run a cycle detector over the graph.
You can also determine that _some_ programs terminate. That is, there is a class of recursive programs that the compiler can look at and say "yes this terminates". Where it fails is that the programs that it says "no" to may still terminate. (So it's a "yes" or "maybe".)
Languages that I've worked with that do this are Lean4, Idris2, and Agda. It's needed for dependent type checking as you only want to run total functions at the type level (to ensure type checking terminates).
Idris will build the call graph as you described and analyze whether values get structurally smaller as they pass through any cycles in the graph. (Also lexicographical stuff like "arg1 gets smaller or arg1 stays the same and arg2 gets smaller".)
I don't know the details of Agda.
Lean has a couple of things that it tries: detect straight up structural recursion, detect general recursion where an argument gets smaller, and it also lets you provide a function on the args for what gets smaller (e.g. length - ix) and a proof that it gets smaller.
I gave this a try with a heap implementation that I wrote. I worked through the proof and hit a wall having to show 0 < 0. It turned out that I had an off-by-one error (I was doing the math for a starts at 1 array). Once I fixed that, I got my proof and the compiler certified that it was total.
Writing proofs is not something your average programmer would want to do for the average program, but I think there is some utility in the compiler being able to say "yes this terminates" or "maybe this doesn't terminate".
Even without object-oriented dynamic dispatch, if the language supports closures or function pointers, you still lose the ability to statically analyze all call targets.
I'm comfortable saying that any direct use of function pointers counts as dynamic dispatch, unless your language's semantics for function pointers are especially strict or static. :)
As for closures, I'm not entirely convinced; closures in Rust don't support recursion because they're lexically-scoped (unless "something something y-combinator", which I confess I don't grasp), and otherwise closures are (usually) just as statically-dispatched as any other function call.
Yes, I wasn't sure if by "dynamic dispatch" you mean "object-oriented polymorphic method calls" or more generally any kind of indirect calls which would include calls through function pointers.
Once you have callsites where you can't resolve the target function statically, you've lost the ability to statically prove the absense of stack overflows.
With Rust, I think methods on trait objects should be enough dynamic dispatch to make it impossible to prove the absence of stack overflows. But I'm not enough of a Rust programmer to know for sure.
Yes, perhaps "indirect call" would better capture my thinking here rather than "dynamically dispatched". :)
> With Rust, I think methods on trait objects should be enough dynamic dispatch to make it impossible to prove the absence of stack overflows.
Well, trait objects are absolutely dynamically-sized types, but in order to store them on the stack you'd need to stuff them behind a Sized pointer type. But there might be other strange edge cases that prevent the ability to guarantee the absence of stack overflows (to say nothing of the fact that stack size differs between platforms).
> Well, trait objects are absolutely dynamically-sized types, but in order to store them on the stack you'd need to stuff them behind a Sized pointer type.
I don't think the question here is about Sized vs. !Sized, but instead about the analyzability of the program's control flow. Aside from layout information, a trait object's vtable is literally just an array of function pointers. So since the target of the dynamic dispatch can only be computed at runtime, proving that it is never recursive can only be done with escape analysis of all trait objects, alongside all function pointers.
(Also, you're correct that Rust does not support directly recursive closures; you can use opaque types to get around the naming problem, but the compiler sees that the closure type becomes cyclic. At least one closure in the chain would have to use dynamic dispatch.)
It doesn't remove it completely: if you have strong type safety on your dynamic dispatch and function pointers, you can use that to restrict the possible control flow. You can also constrain things further if you can relate objects or function pointers passed into a particular function to a callsite. But it does rely on whole-program analysis and while you can make an analysis that will either find the full callgraph or report an error you can't make it accept all valid inputs and reject all invalid ones (because this would still basically reduce to the halting problem).
In practice it's often close enough: I have a hacked-together static stack analysis tool I use for an embedded system and it can deal with function pointers used for callbacks with basically one additional annotation (basically saying "any function passed in as a pointer to this function can be called from this other function"), and it works despite not actually having all the information the compiler would have. I would not however expect it to work on an arbitrary application, especially one which pulls in many libraries, which was not designed with at least some attention to allowing this kind of analysis in mind.
> With exclusively static dispatch I feel like it should be possible to unconditionally detect at least the presence of recursion at compile-time,
That's true, and Rust as a language does do so, but in case of recursion for `async` function rust itself suggests to go the `dyn` route. Adding more to the post, it seems that the use of `async-trait` was the reason that they didn't have any choice in the matter to choose static dispatch, as the language as a whole doesn't support async traits, (just yet! ^-^)
I haven't thought about it closely enough to know whether or not it's feasible to detect recursion in this specific case of dynamic dispatch (compilers are certainly capable of devirtualization, after all). However, any time you see a `dyn Foo` in Rust, any method called on it will be dynamically-dispatched (unless the aforementioned devirtualization optimization happens to kick in): https://doc.rust-lang.org/std/keyword.dyn.html
We are not calling a method on a `dyn Foo`. The type in the original example is statically known to be `KafkaWrapper`. The reduced example case isn't even a method -- it's just an ordinary function: