Tail recursive bind

Stream: lean4

[Juan Pablo Romero]

I'm curious about a recent change to mapM:
image.png

the part do loop as ((← f a)::bs) is the same as bind (f a) fun b => loop as (b :: bs) right?

How is that tail recursive? (as bind is the last expression of the function call, not loop).

[Leonardo de Moura]

Quick remarks:

• We specialize mapM for different monads.
• StateT.bind, ExceptT.bind, ReadetT.bind, ... are all inlined by the code generator.
• The specialized mapM is tail recursive for these commonly used monads. This is not true for every monad, but it is true for the ones we use most of the time.

[Mario Carneiro]

Basically, for that expression to be tail recursive you need bind a f to call f in tail position, and this is true for all the standard monads except List and the CPS monadsStateCpsT and ExceptCpsT

[Juan Pablo Romero]

I see... so it is tail rec because after f a is evaluated and the resulting value b passed to the lambda, the resulting expression loop as (b :: bs) is in tail position and can be evaluated without having to keep any stack information around?

[Mario Carneiro]

well, like Leo said it is also required for all the intermediate stuff to get inlined for it to be syntactically recognized as a tail recursion, but semantically yes that's what's happening

[Juan Pablo Romero]

got it, thanks!