Linear and Affine Typing of Continuation-Passing Style
Joshua James Berdine · 2013
In this dissertation we show that linear and affine type systems for continuation-passing style support correct and tight refinements of standard continuation semantics. In particular, a wide variety of control constructs admit typing disciplines which ensure linear or affine use of the control context in their continuation semantics. This refinement of standard continuation semantics using restricted types is an exploitation of the stylized use of continuations many control behaviors exhibit. Continuations are the raw material of control and can be used to explain a wide variety of control behaviors, including calling/returning (procedures), raising/handling (exceptions), jumping/labeling (goto and labels), process switching (coroutines), backtracking (amb and fail), and capturing/invoking first-class continuations (call/cc, or callcc and throw). However, in all but the last case, continuations are not themselves intrinsic to the control construct, instead they are “behind the scenes, ” implementing the control construct. In other words, except for first-class continuations, each control behavior is simply an idiom of continuation usage, and hence the continuations are used in a stylized fashion. Linear or affine use of control contexts; by which we mean, roughly, that control