Zulip Chat Archive

Stream: lean4

Topic: Constant-stack monadic loops


view this post on Zulip Zygimantas Straznickas (Mar 23 2021 at 03:16):

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.

view this post on Zulip Sebastian Ullrich (Mar 23 2021 at 07:49):

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;
      }
    }
  }
}

view this post on Zulip Zygimantas Straznickas (Mar 23 2021 at 13:24):

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.

view this post on Zulip pcpthm (Mar 23 2021 at 18:21):

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

view this post on Zulip Sebastian Ullrich (Mar 23 2021 at 18:24):

Did you mean to link to the Windows handler?

view this post on Zulip pcpthm (Mar 23 2021 at 18:24):

oops, different line. It is Linux

view this post on Zulip Sebastian Ullrich (Mar 23 2021 at 18:25):

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

view this post on Zulip Sebastian Ullrich (Mar 23 2021 at 18:26):

(I've never seen that happen fwiw)

view this post on Zulip pcpthm (Mar 23 2021 at 18:26):

Perhaps unoptimized build has larger stack frames?

view this post on Zulip Sebastian Ullrich (Mar 23 2021 at 18:31):

It definitely does, but that still sounds excessive

view this post on Zulip Sebastian Ullrich (Mar 23 2021 at 18:32):

Whoops, the 5000 bytes are on Windows

view this post on Zulip Sebastian Ullrich (Mar 23 2021 at 18:33):

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

view this post on Zulip Sebastian Ullrich (Mar 23 2021 at 18:38):

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

view this post on Zulip pcpthm (Mar 23 2021 at 18:40):

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

view this post on Zulip Zygimantas Straznickas (Mar 24 2021 at 02:39):

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


Last updated: May 07 2021 at 13:21 UTC