Stream: lean4

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.

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


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.

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

Sebastian Ullrich (Mar 23 2021 at 18:24):

Did you mean to link to the Windows handler?

pcpthm (Mar 23 2021 at 18:24):

oops, different line. It is Linux

Sebastian Ullrich (Mar 23 2021 at 18:25):

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

Sebastian Ullrich (Mar 23 2021 at 18:26):

(I've never seen that happen fwiw)

pcpthm (Mar 23 2021 at 18:26):

Perhaps unoptimized build has larger stack frames?

Sebastian Ullrich (Mar 23 2021 at 18:31):

It definitely does, but that still sounds excessive

Sebastian Ullrich (Mar 23 2021 at 18:32):

Whoops, the 5000 bytes are on Windows

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

Sebastian Ullrich (Mar 23 2021 at 18:38):

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

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

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