Sure, and thus inlining does not always work. To be clear, what I probably should have said was beta reduction, but I wanted to keep the terminology of the op.

Sure, and thus inlining does not always work. To be clear, what I probably should have said was beta reduction, but I wanted to keep the terminology of the op. The point being that one has to be aware of state in order to execute an inline/beta reduction. In pure and total[0] code the above can only ever change the execution speed, never the meaning. [0] And of course "pure and total" just means "pure" since non-termination is an effect.