4 ms·

The reduction rules copied from Racket's docs: (reset val) => val (reset E[(shift k expr)]) => (reset ((lambda (k) expr)

The reduction rules copied from Racket's docs: (reset val) => val (reset E[(shift k expr)]) => (reset ((lambda (k) expr) (lambda (v) (reset E[v])))) ; where E has no reset E is the current-continuation of the expression, and the comment is an invariant to be held. And I think call/cc is this: E[(call/cc k expr)] => ((lambda (k) expr) (lambda (v) E[v])) So imagine a stack like this: g h call/cc my-fun this captures the whole stack. And now imagine: g reset h shift my-fun this only captures h (see how it moves the E in the reduction rules and wraps it in reset). So if I try to store k from shift and call it at a later time it won't reach g, but doing the same with call/cc it would reach g.

gpderetta 5y ago
Thanks I think I did get that much, but your example still helps a bit. Some questions: - how does (both formally and from an implementation point of view) does shift find the corresponding reset? Does it relies on some sort of dynamic scoping or does the reset need to be lexically visible from the shift call? It doesn't help that in all the examples shift and resets are always called in the same expression (with shift in a lambda). - Related to the above, how does typing work? Is the captured delimited continuation typed (i.e. does it take parameters of a specific type and returns typed values), and if so, does the typing of shift and reset need to match (racket is dynamically typed so this is not an issue there of course). I have no formal language background, I just implement coroutines and (one shot) continuations for fun (in C++), so the key to my understanding is from an implementation point of view. edit: from a comment elsethread it seems that I should look into effect systems.
- the-smug-one 5y ago
  Algebraic effect system = Statically typed delimited continuations, as your edit shows :-). It's dynamically scoped, which is the same as the lexical scope in the untyped lambda calculus. But yes, that is really annoying. Example from Racket REPL: > (require racket/control) > (define f (lambda () (shift k (k 5)))) > (reset (f)) 5
thealig 5y ago
i looked up the racket docs to understand shift/ reset, and stumbled upon a litany of control structures. One is prompt/control, which has almost the same reduction rule.. (prompt E[(control k expr)]) => (prompt ((lambda (k) expr) (lambda (v) (E[v])))) the last reset is the difference, but it seemingly makes no difference, they are interchangeable.

gpderetta 5y ago

Thanks I think I did get that much, but your example still helps a bit. Some questions: - how does (both formally and from an implementation point of view) does shift find the corresponding reset? Does it relies on some sort of dynamic scoping or does the reset need to be lexically visible from the shift call? It doesn't help that in all the examples shift and resets are always called in the same expression (with shift in a lambda). - Related to the above, how does typing work? Is the captured delimited continuation typed (i.e. does it take parameters of a specific type and returns typed values), and if so, does the typing of shift and reset need to match (racket is dynamically typed so this is not an issue there of course). I have no formal language background, I just implement coroutines and (one shot) continuations for fun (in C++), so the key to my understanding is from an implementation point of view. edit: from a comment elsethread it seems that I should look into effect systems.

the-smug-one 5y ago
Algebraic effect system = Statically typed delimited continuations, as your edit shows :-). It's dynamically scoped, which is the same as the lexical scope in the untyped lambda calculus. But yes, that is really annoying. Example from Racket REPL: > (require racket/control) > (define f (lambda () (shift k (k 5)))) > (reset (f)) 5

thealig 5y ago

i looked up the racket docs to understand shift/ reset, and stumbled upon a litany of control structures. One is prompt/control, which has almost the same reduction rule.. (prompt E[(control k expr)]) => (prompt ((lambda (k) expr) (lambda (v) (E[v])))) the last reset is the difference, but it seemingly makes no difference, they are interchangeable.