Presented by Sam Tobin-Hochstadt
Transcribed by Mike MacHenry
call/cc reifies and passes the current continuation
to its argument function.
(δ x (call/cc (λk.k))
E[(abort v)] => v
E[(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]))))
abortin terms of C
(abort x) => (c (λa.x))
call/ccin 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
(% ... (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?
(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
((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]))]