Jason (jcreed) wrote,

Sorted out some issues with the philly apartment. Looks like the current plan is to pick up the truck a week from today, and actually do the drive the following day, so that I arrive during normal business hours so I can actually pick up keys at the office.

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.
Tags: continuations, moving, social

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    More things to add to the "chord progressions that aren't cliches-I-already-know-about nonetheless covertly appearing in multiple places" file.…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment