4 ms·

Is this the case with all statically typed languages? I think I have faced the same issue with PureScript (PS: I'm a contributor)

kibwen 3y ago
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.)
- duped 3y ago
  > 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.
  - kibwen 3y ago
    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.
    - dunham 3y ago
      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".
- munificent 3y ago
  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.
  - kibwen 3y ago
    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.
    - munificent 3y ago
      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.
      - kibwen 3y ago
        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).
- hoosieree 3y ago
  I'm not an expert on fuzzing, but I think a fuzzer would be able to discover this issue.
  - richardwhiuk 3y ago
    Any UT of the function would have caught this issue.
  - kibwen 3y ago
    Sure, but fuzzers are best-effort heuristics, rather than a static guarantee of correctness.
- loeg 3y ago
  I don't think the recursion in this case is dynamically dispatched. It returns a dyn Future, but that isn't the same thing.
  - kibwen 3y ago
    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 https://doc.rust-lang.org/std/keyword.dyn.html
    - loeg 3y ago
      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: fn do_something() -> Pin<Box<dyn Future<Output = ()>>> { Box::pin(async { do_something().await }) } (The infinite recursion happens before anything is ever returned --- the return type is irrelevant.)
      - thethirdone 3y ago
        > (The infinite recursion happens before anything is ever returned --- the return type is irrelevant.) This is not true, the closure is not actually called until the future is awaited. Each instance of do_something does actually return.
- cat-whisperer 3y ago
  > 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! ^-^)

kibwen 3y ago

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.)

duped 3y ago
> 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.
- kibwen 3y ago
  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.
  - dunham 3y ago
    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".
munificent 3y ago
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.
- kibwen 3y ago
  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.
  - munificent 3y ago
    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.
    - kibwen 3y ago
      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).
hoosieree 3y ago
I'm not an expert on fuzzing, but I think a fuzzer would be able to discover this issue.
- richardwhiuk 3y ago
  Any UT of the function would have caught this issue.
- kibwen 3y ago
  Sure, but fuzzers are best-effort heuristics, rather than a static guarantee of correctness.
loeg 3y ago
I don't think the recursion in this case is dynamically dispatched. It returns a dyn Future, but that isn't the same thing.
- kibwen 3y ago
  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 https://doc.rust-lang.org/std/keyword.dyn.html
  - loeg 3y ago
    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: fn do_something() -> Pin<Box<dyn Future<Output = ()>>> { Box::pin(async { do_something().await }) } (The infinite recursion happens before anything is ever returned --- the return type is irrelevant.)
    - thethirdone 3y ago
      > (The infinite recursion happens before anything is ever returned --- the return type is irrelevant.) This is not true, the closure is not actually called until the future is awaited. Each instance of do_something does actually return.
cat-whisperer 3y ago
> 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! ^-^)