Constant-stack monadic loops

Stream: lean4

[Zygimantas Straznickas]

I have the following function that I want to execute in constant stack:

partial def serve (receiveMsg: IO Request) (emitMsg : Response → IO Unit) : IO Unit := do
  let msg ← receiveMsg -- ping?
  if msg.stop then
    return
  emitMsg arbitrary -- pong
  serve

(In and imperative language this would just be a while loop). Experimentally verified, as compiled right now it's not constant-stack. I'm not an expert in FP but a random StackOverflow answer says that "A monadic computation that refers to itself is never tail-recursive" (https://stackoverflow.com/a/13384300), so naive tail call optimization seems to be out. Haskell seems to solve this by being lazy and using some magic called tail recursion modulo cons. Since Lean isn't lazy, this probably won't work, at least naively.

[Sebastian Ullrich]

How did you verify that?

partial def test : IO Unit := do
  IO.println "test"
  test

lean_object* l_test(lean_object* x_1) {
_start:
  {
    lean_object* x_2; lean_object* x_3;
    x_2 = l_test___closed__1;
    x_3 = l_IO_println___at_Lean_instEval___spec__1(x_2, x_1);
    if (lean_obj_tag(x_3) == 0)
    {
      lean_object* x_4;
      x_4 = lean_ctor_get(x_3, 1);
      lean_inc(x_4);
      lean_dec(x_3);
      x_1 = x_4;
      goto _start;
    }
    else
    {
      uint8_t x_6;
      x_6 = !lean_is_exclusive(x_3);
      if (x_6 == 0)
      {
        return x_3;
      }
      else
      {
        lean_object* x_7; lean_object* x_8; lean_object* x_9;
        x_7 = lean_ctor_get(x_3, 0);
        x_8 = lean_ctor_get(x_3, 1);
        lean_inc(x_8);
        lean_inc(x_7);
        lean_dec(x_3);
        x_9 = lean_alloc_ctor(1, 2, 0);
        lean_ctor_set(x_9, 0, x_7);
        lean_ctor_set(x_9, 1, x_8);
        return x_9;
      }
    }
  }
}

[Zygimantas Straznickas]

By getting a stack overflow when calling that function :) and then looking into generated c. But thanks! Your example looks like a disproof of “A monadic computation that refers to itself is never tail-recursive” and I want to understand this better so I’ll go dig deeper.

[pcpthm]

I get stack overflow here <https://github.com/leanprover/lean4/blob/ffef5635bb49a7221b36c0f56a4ae9fe93d2cb85/src/Lean/Data/Json/Parser.lean#L131-L148> when lean is compiled without optimization (C compiler option), e.g. nix build .#debug.
(Another issue: the stack overflow handler itself overflows the stack while trying to print message here <https://github.com/leanprover/lean4/blob/0a280793c7b386c7a0b1bb65c3de19dd2c39d814/src/runtime/stack_overflow.cpp#L71>)

[Sebastian Ullrich]

Did you mean to link to the Windows handler?

[pcpthm]

oops, different line. It is Linux

[Sebastian Ullrich]

Ok. So 5000 bytes are not sufficient for printing a simple message? :frowning:

[Sebastian Ullrich]

(I've never seen that happen fwiw)

[pcpthm]

Perhaps unoptimized build has larger stack frames?

[Sebastian Ullrich]

It definitely does, but that still sounds excessive

[Sebastian Ullrich]

Whoops, the 5000 bytes are on Windows

[Sebastian Ullrich]

SIGSTKSZ

    This is the canonical size for a signal stack. It is judged to be sufficient for normal uses.

Who are we to judge I guess...

[Sebastian Ullrich]

If you want to try with 2 * SIGSTKSZ or something, please go ahead

[pcpthm]

To reproduce: Let replay.txt be <https://gist.github.com/pcpthm/05203a0004f3415f066bc909732b0ea6> and lean --server < replay.txt, where lean is nix build .#debug.
Also whether it is printing the Stack overflow detected. Aborting. message seems nondeterministic (sometimes I only get Aborted (core dumped)).

[Zygimantas Straznickas]

Update: solved this by implementing something like https://github.com/purescript/purescript-tailrec (though I'm half sure I could have reused ForIn from stdlib for this instead of creating a new class).