Stack safe Bind

Stream: lean4

[Juan Pablo Romero]

Is it possible to build a stack safe Bind/Monad (a la IO) purely within Lean? or does it require special runtime support?

For example I'd like to write a stack safe function like this:

instance : Monad M where
  pure := ...
  bind := ...

def repeatN (ma: M A) (n: Nat) : M Unit := do
  let _ <- ma
  if n > 0 then
    repeatN ma (n - 1)

[Henrik Böving]

What do you mean by stack safe? That it doesn't kill the program in case it overflows?

[Juan Pablo Romero]

Yeah, I'm trying to avoid stack overflows, basically

[Henrik Böving]

I'd say since it depends highly on compiler optimizations if and how much stack space is used this seems quite impossible to do precisely?

[Kyle Miller]

I think the question here is about whether Lean does tail call optimization for monadic functions

[Juan Pablo Romero]

right

[Chris Bailey]

The CPS monads in Init.Control do (or did). You might also be able to use the loop syntax.

[Juan Pablo Romero]

oh, let me take a look

[Sebastian Ullrich]

I'd say this should just work iff your bind calls the second argument in tail position

[Juan Pablo Romero]

got it. In this case M is a GADT which only captures its arguments:

inductive M : Type -> Type 1 where
...
  | Bind (ma: M A) (f: A -> M B) : M B

and later gets interpreted

def run (m: M A) (callback: A -> IO Unit) : IO Unit := match m with
...
      | .Bind ma cont =>
        run ma $ fun a => run (cont a) callback
...

I guess this is where the Stack Overflow is coming.