Jason (jcreed) wrote,

Hmm. I wonder why we really need the generality of
ω2,ω1 τ = (τ → ω1) → ω2
as opposed to the answer-type-is-ω CPS monad
ω τ = (τ → ω) → ω

The latter seems to work, in that if I just forcibly unify all the //-annotations on the left with all the //-annotations on the right, things are still vaguely sensible. Is it just so we can treat the continuation-up-to-last-reset has having a kind of let-polymorphism?

For example, I seem to be able to type
"Hello World, today the temperature is " ^ (reset (shift k . Int.toString (k 25))

with a typing derivation sketched by:
k : int -> int |- Int.toString (k 25) : string
k : int -> int // string |- pure (Int.toString (k 25)) : string // string
// int |- shift k . pure (Int.toString (k 25)) : int // string
|- reset (shift k . pure (Int.toString (k 25)) : string
The moral here being that the "real" continuation that that shift captures is an evaluation context that is going to require a string, and yet since it's delimited, it's really only the identity function, and can be safely used at int.

And yet the effective let-polymorphism doesn't seem to be as complete as I might have expected, in that I have to choose the type of k once and for all when I shift, so that
(reset (shift k . (k "Hello ") ^ Int.toString (k 25))

does not appear to be well-typed.
Tags: continuations, math, monads

  • (no subject)

    Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

  • 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