Visited adam and susan and the twins. They're pretty huge for seven months old --- perhaps predictably, given their super-tall immediate ancestry.
Found myself reading a Dybvig, Peyton-Jones, and Sabry paper from 2007 about delimited continuations for no particularly good reason. The punchline seems to be that you can treat delimited continuations much like regular ones (even with dynamic prompts) as long as you choose the appropriately beefed-up CPS-ish monad to work in. It reminded me that I don't off the top of my head know the answer to the following question:
On the one hand, we know how to do CPS in nice higher-order style so that no "administrative redices" ever arise in the first place. One translation takes source-language values to cps-language values (call this latter type cv), and the other takes source-language expressions to something of type (cv → ce) → ce where ce is the type of cps-language expressions, where both arrows are really meta-level functions. That is, the expression translation takes a source expression and a meta-continuation (a cps expression with a cps-value-binding hole) and uniformly outputs a cps expression.
On the other hand, (and a careful discussion of this appears in the paper mentioned) we can cleave apart the CPS translation into two halves: (a) the usual monadic translation that just inserts Circle everywhere in the type, and wedges in a bunch of returns and binds enough to make the type work out and to express the CBV evaluation order, and (b) the instantiation of Circle A with the CPS monad (A → R) → R, and the implementation of return and bind as appropriate.
Question: isn't there a nicer story to tell about the "On the other hand" way of separating CPS into general monadic transform + CPS monad that avoids administrative redices? I feel like I can't just naïvely push the →'s up to the meta-level in the same way.