2 ms·

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

by 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 sago 11y ago

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.