Tail recursion works (sometimes at least) only because we're lucky

[lukaszcz]

The following program works fine with the current setup:

module tailrec;

inductive Nat {
  O : Nat;
  S : Nat -> Nat;
};

mult2acc : Nat -> Nat -> Nat;
mult2acc O acc := acc;
mult2acc (S x) acc := mult2acc x (S (S acc));

mult2 : Nat -> Nat;
mult2 x := mult2acc x O;

pow2acc : Nat -> Nat -> Nat;
pow2acc O acc := acc;
pow2acc (S x) acc := pow2acc x (mult2 acc);

pow2 : Nat -> Nat;
pow2 x := pow2acc x (S O);

axiom Action : Type;
compile Action {
  c ↦ "int";
};

axiom ignore : Nat -> Action;
compile ignore {
  c ↦ "ignore";
};

foreign c {
  int ignore(void* x) { return 0; \}
};

main : Action;
main := ignore (pow2 (pow2 (S (S (S (S O)))))); -- 2 ^ 16 = 65536

end;

That's how one implements iteration in an eager functional programming language. The pow2 and mult2 function invocations should use constant stack space. For this tail call elimination in the compiler is necessary.

It works now, because we pass '-Oz' to 'clang' and tail call elimination is one of the optimisations at the C level. However, if one removes Compile.hs:163, then we get:

% minijuvix compile tailrec.mjuvix
% wasmer tailrec.wasm             
error: failed to run `tailrec.wasm`
│   1: RuntimeError: out of bounds memory access
╰─▶ 2: heap_get_oob

Confusingly, the message is about the heap, but it's definitely the stack. With tail call optimisation it runs fine for 2 ^ 32.

The problem is that the C standard does not guarantee that tail call elimination be performed -- it's optional. There is no guarantee that a different C compiler will perform it. Moreover, because of the intricacies of the C memory model, tail call detection is somewhat involved in C, sometimes the compilers miss it, etc.

For an eager functional programming language compiled "ML-style" tail call elimination is not optional.

It's not possible to implement tail call elimination with standard C if one is translating source language functions directly to C functions, and source function calls to C function calls, because C function calls may grow the stack.

I see two ways out of this:

1. assume that we'll always be using 'clang' or another compiler with tail call optimisation, and the extent to which the compilers do perform tail call elimination will always be sufficient,
2. implement a "proper" C runtime for MiniJuvix.

I lean toward the second solution. It is more robust long-term and more "standard". I don't believe one can do a "direct" (i.e., function to function) translation from a functional programming language to C without running into more problems later. For one thing, with the first solution we're definitely going to have portability issues when trying to implement a garbage collector (necessary long-term).