The Cat Keeps Coming Back
Today, got a CPS transformation kind of working on a toy lambda-calculus. Something's snagging me up, and it's the collision of CPS with laziness.
As a test term, I'm using variations of this:
call_cc (lambda e. 1 + (if P then 5 else (e 5)))
What should happen? if P is true, we should take the first branch and return 5 from the if, which is then incremented and returned to the top level--the result is "6". If P is false, then we take the (e 5) branch. e is the continuation sent by call_cc, which is effectively the toplevel, so applying e to 5 should simply return 5 to the toplevel and drop everything else.
But in my pure lazy lambda calculus, I don't have a way to tell the interpreter to "drop" everything which is irrelevant. Invoking the continuation should never return, but in this pure setting, there's no natural way to prevent it from returning. I faked it by creating a primitize Print, which prints a value and returns Bot; Bot is like die: evaluating any application that involves Bot just returns Bot, which gives me a way to fake the non-returning quality of the toplevel.
Using Print in the toplevel continuation, I was able to get the desired behavior: by varying P I can get either 6 or 5 as the result of the expression. That feels good! Continuations are working!
Still, this can't be the standard way to do it. How does a continuation "never return" in pure lambda-calculus?