Presented by Sam Tobin-Hochstadt
Transcribed by Mike MacHenry
call/cc reifies and passes the current continuation
to its argument function.
A review:
(δ x (call/cc (λk.k))(x (λy.1))(void)(x (λy.2))1
call/ccE[(abort v)] => vE[(call/cc v)] => E[(v (λx. (abort E[x])))]The abort is necessary here because otherwise we execute continuations twice by returning to a context after invoking a continuation
E[(C v)] => (v (λx.(C (λd.E[x]))))abort in terms of C(abort x) => (c (λa.x))call/cc in terms of C(call/cc x) => (λr.(C (λk. (k (r k)))))This avoids the the complications with abort. Throws away the current continuation and returns the applied value to that continuation.
E[(F v)] => (v (λx.E[x]))(abort x) => (F (λa.x))Saves the whole continuations a gives it to you.
We abort so we don't run the rest of the computation twice because
the continuation of call/cc is just what is reified and executed.
Some times it's inefficient to know the whole rest of the computation
when you just want to exit a while loop.
(% ... (control (λk ...) ...) ...)
Only grabs the coninuation up til the prompt %
E[(% F[(control v)])] => E[(% (v (λx.F[x])))](% (add1 (control (λk. (k (k 3))))))
Q: What does this do?
A: 5
(reset ... (shift (λk. ...)) ...)
E[(reset F[(shift v)])] => E[(reset (v (λx.(reset F[x]))))](spawn (λk.e)) gives to its argument a control
operator a lot like F but its delimited by the spawn that created
it.
((spawn (λk.k)) 3) doesn't make sense
(spawn (λk. (spawn (λl. (k 3))))) if we
shadow it's different
(splitter (λabort,call/pc. ...)) abort throws
away context and evaluates in splitter.
E[(splitter (λa,c.F[(abort e)]))] => E[(e)]E[(splitter (λa,c.F[(c v)]))] => E[(splitter (λa,c.F[(v (λx.F[x]))]))]call/pc does not abort so it it's a function that you can apply and control passes back to where you invoked it from
(% ... (λx,k ...) ...) allows you to catch
exceptions and put in for their place essencially retry the computation
that threw it.
E[(% F[(f-control v)] v)] => E[v' v (λx.F[x]))]