Is this the case with all statically typed languages? I think I have faced the same issue with PureScript
(PS: I'm a contributor)
(PS: I'm a contributor)
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.
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.
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".
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.
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.
> 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).
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.)
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.
fn do_something() -> Pin<Box<dyn Future<Output = ()>>> {
Box::pin(async { do_something().await })
}
This is not true, the closure is not actually called until the future is awaited. Each instance of do_something does actually return.
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! ^-^)