[tel]

Ever used CPS style? Instead of producing values and passing them back to callers you provide continuations to functions and then they never return, merely calling the continuation instead. It turns out that this can save a lot of stack space and it also turns out that you can convert any program into this style should you choose.

It might not be exactly clear why CPS is equivalent to "direct" style. The answer is the Yoneda Lemma.

Yoneda goes further. Normally you could maybe notate a CPS style function as follows

    (a -> *) -> *

where `a` is the type of the value the computation will pass to the continuation function (the first argument here) and * is a special type indicating "will never return". We can generalize this slightly as

    forall x . (a -> x) -> x

which enables us to talk about CPS'd code in a slightly more general way by not stating exactly what the continuation does—it produces some kind of value, which might be the "will never return" value, and the CPS'd function just needs to evaluate it because the forall is positioned such that it can't know what `x` is. This gives more power to the user of CPS'd functions.

We can generalize it again by writing

    forall x . (a -> x) -> F x

which gives more power to the implementer of the CPS'd function by letting them return some kind of "effect structure" along with calling the handler. The effect structure is fixed ahead of time but lets us talk about

    * calling the continuation multiple times
    * returning failure via exceptions
    * producing side effects
    * producing default values when no `a` ever existed
    * etc.

And in this most general setting Yoneda still comforts us that this is just equivalent to the "direct" form

    F a

[kazinator]

I think it's clearer if you don't bring in the lemma. Calling the continuation is the same as returning a value: both are just a jump that restores the stack pointer and communicates a value. (The continuation just keeps the stack below the stack pointer instead of discarding it.) (Could it be that it's because continuations have certain properties that they fall under the lemma?)

The commutative diagrams, rather, remind me of diagrams that I remember from chemistry. We can go from this molecule to that one via this path or that one, and the energy deltas are the same.

Speaking of continuations, I'm currently looking at porting the trick used by some OCaml people of doing delimited continuations on the C stack, into my own language. It's pretty neat: just copy the C stack into a closure-like object, and then when you need to invoke the continuation, swap that segment back onto the regular linear stack (into a stable space prepared using alloca). Rebuild some exception handling chains through this new pieces of stack, and then invoke the thing using an exception (ultimately a longjmp). When it is done running, you can blow it away. All permanent effects are in external environments that are on the heap. The next time you call into it, you just copy it in the same way.

I'm unclear on how you can do a longjmp to something that has been copied elsewhere on the stack relative to its original location. I mean, the jmp_buf probably has an absolute stack pointer in it which it restores. I have to look at their code again; the obvious hack is to scan the jmp_buf for values that look like pointers into the stack area and adjust those values.

I implemented a stack copying hack once to get a 64 bit Linux kernel on MIPS to call into 32 bit firmware, passing ordinary local variables (whose addresses are 64 bit values on a 64 bit stack) to the firmware functions. I copied the kernel thread's stack into a buffer 32 bit addressable space. Then I adjusted all internal pointers within that stack to point to the correct places in the new location. The threads's pointer was then thunked into that space around the call to the firmware. The firmware API wrapper was then seeing data addresses whose lowest 32 bits could be passed down to the firmware routines via 32 bit registers and still point to the correct data. Of course, a reverse copy from the faked stack was then done to retrieve any results which the firmware routine wrote into local buffers. This worked well enough that I was able to expose boot firmware environment variables through a /proc interface (even making it writable!) Based on such past experience, I'm confident I can do this delimited continuation hack.

[throwaway000002]

> I think it's clearer if you don't bring in the lemma.

Well of course it's clearer, it's because you're working with specific example, whereas Yoneda applies in a very general setting, you just have to see how you can "squint" and see the general setup in the specific case.

People always talk about a category Hask, but you can easily imagine a category "C" in an analogous way. You can also imagine an "SSA" category of a static single-assignment intermediate language of a compiler. Compilation would be a functor from C to SSA. Likewise you can consider an (endo)functor from C to C which turns a function from direct style to CPS, and then run the compiler to get SSA. You can then ask is the SSA generated in both steps the same "semantically". Actually proving that in all its gory detail is simplified by making the right setup as explicated by user tel and then applying the Yoneda lemma at the right moment to conclude the proof.

More interestingly you can ask questions like does an SSA optimisation, an (endo)functor on SSA correspond to some optimisation in C that could be a source-to-source transform.

Etc, etc.

The purpose of mathematical abstraction is simplification, even though it may transmogrify the concrete into a seemingly unpalatable form.

[tel]

Outside the topic of admittedly really cool delcont stuff:

The way you refer to the value and the CPS'd value as the same is by referring to their effects in stack machine semantics as the same. This makes your intuition non-transferrable to other semantics (lacking a clear CS example off the top of my head, I'll just throw out the usual trick of asking: does this work the same on a GPU? I'm confident there's a Yoneda analogue there).

Studying CT is completely extra-curricular as far as I'm concerned and I could never recommend it as a way to implement or use CPS, but understanding, for certain rather aggressive values of "understand" I feel comes from nearly no other pathway. It's entirely too beautiful and simple (for certain mathematical values of "simple") to escape.

Also the commutative diagrams are pretty much exactly the same as the chemistry ones you're talking about. Both are just ways of writing down systems of equations that are quite hairy to write out "long form".