3 ms·

I think how a continuation is represented is an implementation detail that depends on many things, one of them being the ambient programming language and typing

by mafribe 11y ago

I think how a continuation is represented is an implementation detail that depends on many things, one of them being the ambient programming language and typing system (which may enforce e.g. linear usage of continuation). But in all cases what you do with a continuation is the same, you define a point in the computation (that's what callcc does) that you can go back to (by executing throw). That's why I like to explain callcc / throw by analogy with goto. Once that behaviour is clear, the question of representation is natural and comprehensible.

sago 11y ago
Can you give an example of a 'linear usage of continuation', that doesn't have the continuation be a data structure (or data type)? I'm curious. The question is genuine, not passive aggressive, I don't understand the distinction you're making there.
- mafribe 11y ago
  This is a very good question. Continuations can be used to explain a wide variety of program control such as calling/returning (procedures), raising/handling (exceptions), jumping/labeling (goto and labels), process switching (coroutines), backtracking (amb and fail), and capturing/invoking first-class continuations (callcc and throw). An example of using the full power of continuations is the notorious argfc function [1]: callcc lambda k.(throw k (lambda x.(throw k lambda y.x))) This is the classic example of calling a function once, but returning twice. The function argfc normalises to a lambda-abstraction, but, as [2] investigates, distinguishes programs by application that are indistinguishable in the absence of continuations: (lambda x.(x 1);(x 2)) argfc = 1 but (lambda x.lambda y.(x 1);(y 2)) argfc argfc = 2 with M;N being the sequential composition of M and N, binding more tightly than lambda-abstraction. As you know, the reason is that continuations carry information about contexts that may be returned (jumped) to later. If we use continuations linearly (i.e. exactly once) or affinely (at most once), such forms pathological behaviour cannot occur, so implementations might be easier. In particular, special cases of continuation use such as function call/return and exception throw/catch do not require such duplication of continuations, so can be implemented much more easily than general continuations. It is the completely unrestricted nature of full callcc/throw that requires the implementation to capture the whole call stack. [1] H. Thielecke, Continuations, functions and jumps. [2] J. G. Riecke, H. Thielecke, Typed Exceptions and Continuations Cannot Macro-Express Each Other.

by mafribe 11y ago

sago 11y ago

Can you give an example of a 'linear usage of continuation', that doesn't have the continuation be a data structure (or data type)? I'm curious. The question is genuine, not passive aggressive, I don't understand the distinction you're making there.

mafribe 11y ago
This is a very good question. Continuations can be used to explain a wide variety of program control such as calling/returning (procedures), raising/handling (exceptions), jumping/labeling (goto and labels), process switching (coroutines), backtracking (amb and fail), and capturing/invoking first-class continuations (callcc and throw). An example of using the full power of continuations is the notorious argfc function [1]: callcc lambda k.(throw k (lambda x.(throw k lambda y.x))) This is the classic example of calling a function once, but returning twice. The function argfc normalises to a lambda-abstraction, but, as [2] investigates, distinguishes programs by application that are indistinguishable in the absence of continuations: (lambda x.(x 1);(x 2)) argfc = 1 but (lambda x.lambda y.(x 1);(y 2)) argfc argfc = 2 with M;N being the sequential composition of M and N, binding more tightly than lambda-abstraction. As you know, the reason is that continuations carry information about contexts that may be returned (jumped) to later. If we use continuations linearly (i.e. exactly once) or affinely (at most once), such forms pathological behaviour cannot occur, so implementations might be easier. In particular, special cases of continuation use such as function call/return and exception throw/catch do not require such duplication of continuations, so can be implemented much more easily than general continuations. It is the completely unrestricted nature of full callcc/throw that requires the implementation to capture the whole call stack. [1] H. Thielecke, Continuations, functions and jumps. [2] J. G. Riecke, H. Thielecke, Typed Exceptions and Continuations Cannot Macro-Express Each Other.