CitationsSee all >20 References
10.91University of TsukubaAbstractWe study the dynamic control operators for delimited contin- uations, control and prompt. Based on recent developments on purely functional CPS translations for them, we introduce a polymorphically typed calculus for these control operators which allows answer-type mod- ification. We show that our calculus enjoys type soundness and is com- patible with the CPS translation. We also show that the typed dynamic control operators can macro-express the typed static ones (shift and reset), while the converse direction is not possible, which exhibits a sharp contrast with the type-free case.Discover the world's research13+ million members100+ million publications700k+ research projects
Typed Dynamic Control Operatorsfor Delimited ContinuationsYukiyoshi Kameyama and Takuo YonezawaDepartment of Computer Science, University of Tsukubakameyama@acm.org, yone@logic.cs.tsukuba.ac.jpAbstract. We study the dynamic control operators for delimited contin-uations, control and prompt. Based on recent developments on purelyfunctional CPS translations for them, we introduce a polymorphicallytyped calculus for these control operators which allows answer-type mod-ification. We show that our calculus enjoys type soundness and is com-patible with the CPS translation. We also show that the typed dynamiccontrol operators can macro-express the typed static ones (shift andreset), while the converse direction is not possible, which exhibits asharp contrast with the type-free case.Keywords: Type System, Delimited Continuation, Dynamic ControlOperator, CPS Translation, Polymorphism, Expressivity.1 IntroductionDelimited continuations represent not the rest of the computation as with tradi-tional continuations [18], but only part of the rest of the computation. As such,delimited continuations have been used to model backtracking in contrast totraditional continuations that are used to model jumps.In direct style, traditional continuations are accessed with control operatorssuch as call/cc. There is, however, more variety for delimited continuations:–Felleisen [12] proposed a control delimiter to signify part of an evaluationcontext, or a delimited continuation. This lead to the new control operatorscontrol and prompt, which are called dynamic control operators.–Danvy and Filinski discovered that delimited continuations are supported byan already existing formalism of 2CPS, the image of iterated CPS transla-tions. They proposed new control operators shift and reset in the direct-style counterpart [9]. They are called static control operators.Since these proposals, the static control operators have been intensively studiedwhile the dynamic ones are relatively less studied. For shift/reset, there area number of theoretical results [13, 14] as well as useful examples in partialevaluation, one-pass CPS translation, and mobile codes, while we do not findmany corresponding works for control/prompt in the literature, partly due tothe difficulty in reasoning about the dynamic features of control/prompt.Recently, several authors have started to obtain better understanding for dy-namic ones, and to connect dynamic and static ones. Shan [7] macro-expressed
control and prompt in terms of shift and reset using recursive types. (Seealso Kiselyov’s work [15].) Biernacki, Danvy, and Millikin [6] derived a CPStranslation for control and prompt from a definitional abstract machine, andgave another encoding of control/prompt by shift/reset. Dybvig, PeytonJones, and Sabry [11] gave a uniform monadic framework for delimited continu-ations including control/prompt. However, no work has studied the direct-styletype system for control/prompt in a way comparative to the type system forshift/reset. The proposed encodings were done in either type-free or recur-sively typed settings,1and the proposed CPS translations assumed a restricteddirect-style type system in that the control effect of “answer-type modification”was not allowed. We think this effect is indispensable for delimited continuations,for instance, it is needed to type the printf function in direct style [8, 1].In this paper, we propose a direct-style type system for control and prompt,which allows answer-type modification, does not need recursive types, and hasML-like let-polymorphism. We derive the type inference rules from the typestructure for the CPS translations for control and prompt recently developed bythe above mentioned works. The type system in this paper is a proper extensionof that in our previous work [20], which does not allow answer-type modification.We show that our type system enjoys Subject Reduction and Progress properties,and that types are preserved by the CPS translation. The first two propertiesconstitute type soundness, and the third property is necessary for a semanticalstudy.As an application of our type system, we compare the expressivity of typedcontrol/prompt and that of typed shift/reset. In the type-free setting, theyare known to be equally expressive [7, 15, 4, 6]. However, there exists a big asym-metry in the complexity of these encodings, and a question remained whethercontrol/prompt is strictly more expressive than shift/reset under an ap-propriate typed setting (without recursive types). In this paper we answer thisquestion. Namely, we show:–typed control/prompt can macro-express typed shift/reset, while–typed shift/reset cannot macro-express typed control/prompt,where the type system for shift/reset is the most expressive type system byAsai and Kameyama [2]. This result contrasts with the type-free case.This paper is organized as follows: in Section 2 we briefly explain the controloperators for delimited continuations, and in Section 3 we review the functionalCPS translation in the literature. The subsequent three sections are original tothis paper: in Section 4 we introduce the type systems for the dynamic controloperators, and in Section 5 we give several properties for the type systems. InSection 6, we compare the expressive power of typed control/prompt with typedshift/reset. Section 8 concludes.1We distinguish (general) recursive types from inductive types in that the formermay contain negative occurrences of the type variable being taken the fixed point,for instance, uX.(X→int) where uis for the fixed point operator.2
fun foo xs =let fun visit nil = nil| visit (x::xs) = visit (shift (fn k =& x::(k xs)))in reset (fn () =& visit xs) endfun bar xs =let fun visit nil = nil| visit (x::xs) = visit (control (fn k =& x::(k xs)))in prompt (fn () =& visit xs) endFig. 1. List-copying and list-reversing functions2 Informal Explanation of control and promptWe begin with the examples by Biernacki et al. [6] listed in Figure 1 written inStandard ML syntax.The functions foo and bar have type int list -& int list, and differin the names for control operators only: shift and reset for the former andcontrol and prompt for the latter. Both shift and control capture evaluationcontexts up to the closest delimiter (reset and prompt, resp.) Given the list[1,2,3], the function foo evaluates as:foo [1,2,3] ?&visit (shift (fn k =& 1::(k [2,3])))&?&let k = &visit o& in 1::(k [2,3]) end&?&1::&visit [2,3]&&?&1::&let k = &visit o& in 2::(k [3]) end&&?...?&1::&2::&3::nil&&& ?[1,2,3]where &... &denotes the delimiter inserted by reset, and &visit o&denotesthe delimited evaluation context (delimited continuation) captured by shiftwith obeing the hole in it. The expression &v&evaluates to vitself when vis avalue, hence the result of this computation is identical to the argument.The evaluation of bar proceeds as follows (the delimiter is denoted by #):bar [1,2,3] ?#(visit (control (fn k =& 1::(k [2,3]))))?#(let k = (visit o) in 1::(k [2,3]) end)?#(1::(visit [2,3]))?#(let k = (1::(visit o)) in 2::(k [3]) end)?#(2::(1::(visit [3])))?...?#(3::(2::(1::nil))) ?[3,2,1]3
The evaluation context captured by control is the whole context since there isno other delimiters. Hence, we obtain a a reversed list as the result of computa-tion.The operational behavior for each set of control operators can be formalizedby reduction rules. Let vand Pdenote a value and a call-by-value evaluationcontext such that no delimiter encloses the hole, resp. Then we have the reductionrules as follows:(For shift/reset)hP[Sc.e]i→hlet c=λx.hP[x]iin ei(For control/prompt) # (P[Fc.e]) →# (let c=λx.P [x]in e)Here Sc.e corresponds to (shift (fn c =& e)), and heito (reset (fn () =&e)) in the ML implementation in the previous subsection. Similarly, # eis(prompt (fn () =& e)), and Fc.e is (control (fn c =& e)).Besides the names for control operators, the only difference between them iswhether the captured delimited continuation has an extra reset or not: λx.hP[x]ifor the former, and λx.P [x] for the latter. This small difference in syntax raisesa big difference in semantics. Suppose Phas other occurrences of shift orcontrol, and the captured delimited continuation is applied to a value vin athen-current continuation Ewhich may have a delimiter that encloses the hole.–In the former, we evaluate E[hP[v]i] in which other occurrences of shiftin Pwill be delimited by this reset (unless they are “escaped” in functionclosures). Namely, the corresponding delimiter for these shift is determinedwhen the delimited continuation is captured.–In the latter, we evaluate E[P[x]] in which other occurrences of controlought to be delimited by prompt in E. (Note that Pdoes not have anyprompt which encloses the hole). Consequently, the corresponding delim-iter for these control is determined not when it is captured, but when thedelimited continuation is used.Hence the former is called static, and the latter is called dynamic by analogy withstatic and dynamic binding in Scheme and Lisp [5]. The static/dynamic natureof control operators has an impact on their implementation. For shift/reset, adelimited continuation can be represented by an ordinary, composable function,which leads to a simple CPS translation [9, 10]. For control/prompt, we needto keep the captured delimited continuations as they are, until they are actuallyused, which needs an extra machinery.3 A CPS translation for control/promptWe regard a CPS translation as the fundamental analysis tool for control oper-ators. For control and prompt, three such translations are known: Shan’s [7],Dybvig, Peyton-Jones, and Sabry’s [11], and Biernacki, Danvy and Millikin’s [6].In this paper we use (a variant of) the last one since it is the simplest. We coulduse Shan’s one as well.4
v::= d|x|λx.e valuee::= v|e1e2| Fc.e |#e|let x=e1in e2|if e1then e2else e3expressionP::= [ ] |P e |vP|let x=Pin e|if Pthen e1else e2pure evaluation contextE::= [ ] |Ee |vE|let x=Ein e|if Ethen e1else e2|#Eevaluation contextFig. 2. Syntax of the language with control/prompt(λx.e)v?e[v/x]if true then e1else e2?e1if false then e1else e2?e2let x=vin e?e[v/x]# (P[Fc.e]) ?# (let c=λx.P [x]in e)#v?vFig. 3. Reduction rulesFigure 2 gives the syntax of our source language where dis constant and xand care variables. The expression Fc.e is a construct for control in whichcis a bound variable. The expression # eis the one for prompt. Variables arebound by λor F, the set of free variables in eis denoted by FV(e), and weidentify α-equivalent expressions. Sequencing a;bis an abbreviation of (λx.b)awith x6∈ FV(b). In a pure evaluation context P, no prompt may enclose its hole[ ], while a (general) evaluation context Eallows such occurrences of prompt.Figure 3 gives call-by-value operational semantics to this language where e[v/x]represents the result of capture-avoiding substitution.Figure 4 defines the CPS translation for this language as a variant of the onegiven by Biernacki et al. The differences are: (1) they gave a 2CPS translationwhch is an iterated translation (its image takes two continuations as its argu-ments), while we use a more traditional 1CPS translation, and (2) we extendthe source language with constant, conditional, and let.The target language of this translation is a call-by-value lambda calculuswith constants, conditional, and let as well as list-manipulating constructs suchas Nil, cons (denoted by ::), append (@) and a destructor (case). Note that thetranslation for let expression is only meaningful for the typed source language(given in the next section), and we have included it in Figure 4 only to savespace. For a type-free source language, we can define it as [[let x=e1in e2]] =[[(λx.e2)e1]].5
[[ ]] : SourceTerm →Cont →Trail →TargetValue[[V]] = λk t. k (V)*t[[e1e2]] = λk t. [[e1]](λm1t1.[[e2]](λm2t2. m1m2k t2)t1)t[[if e1then e2else e3]] = λk t. [[e1]](λm1t1.if m1then [[e2]] k t1else [[e3]] k t1)t[[let x=e1in e2]] = λk t. let x= ([[e1]] θ1Nil)in [[e2]] k t[[# e]] = λk t. k([[e]] θ1Nil)t[[Fc.e]] = λk t. let c=λx k0t0. k x (t@ (k0:: t0)) in [[e]] θ1Nil( )*:SourceValue →TargetValue(d)*=dfor constant(x)*=xfor a variable(λx.e)*=λx k t. [[e]] k tθ1=λx t. case tof|Nil =>x|(k1:: t1)=>k1x t1Fig. 4. 1CPS translation for the language with control and promptLet us see the types in Figure 4, although these types should be consideredinformal, and only for explanation. The types SourceTerm,SourceValue,Cont,TargetValue, are those for terms and values in the source language, and thosefor continuations and values in the target language, resp.The type Trail is new to their CPS translation. Recall that, in order to rep-resent the dynamic behavior of control/prompt, we need to keep the delimitedcontinuations until they are used. A trail is a list of delimited continuations tostore these continuations. Thus, we may informally define Cont and Trail asfollows:Cont =TargetValue →Trail →TargetValueTrail =List(Cont)This “definition” needs recursive types, which will be examined in the nextsection.Next, we look at the term-level translation in Figure 4. For the constructsother than control operators, the translation is the same as the standard (e.g.Plotkin’s) translation except that it passes trails without changing them.The prompt-term # einitializes its continuation and trail: in its translation[[# e]], [[e]] is applied to θ1and the empty trail Nil. The continuation θ1acts asthe identity continuation (the empty evaluation context).The control-term Fc.e captures a delimited continuation (and initializes thecontinuation and the trail): it captures the current delimited continuation kfor6
a future use of c. When cis applied to some value, the captured continuation kis “composed” with the then-current continuation k0. Rather than simply com-posing two delimited continuations, we store (in the trail) the list of all thecaptured delimited continuations except the current one, namely, we extend thethen-current trail t0to a new trail t@ (k0:: t0) and use kas the current continua-tion. Continuations stored in the trail will be used when the current continuationbecomes empty (i.e. θ1).Note that we can easily extend our source language and the CPS translationwith practical language constructs such as the fixed point operator and primitivefunctions.Finally, a CPS translation for a complete program eis defined as [[e]]θ1Nil.4 Type SystemWe introduce a polymorphic type system for control/prompt in this section.Types are an important facility in most programming languages to classify termsand also to ensure a certain kind of safety for computation. We think that, forcontrol/prompt to be used by ordinary programmers, a sound type system isdefinitely needed.4.1 Design of Type SystemOur strategy to construct a type system for control/prompt is basically thesame as that for shift/reset [2]: given a term e, we infer the most general typeof its CPS translation [[e]], and use this type as the type for e. There is, however,two problems in this strategy: (1) the target terms of the CPS translation forcontrol/prompt need recursive types if we assign types, and there is no notionof the most general type in a type system with recursive types, and (2) we needarbitrary many type variables to precisely represent types of the CPS translation.The first problem already appears if we type the identity (delimited) contin-uation θ1. Assuming the type of trails is List(τ) for some τ,θ1must have thetype α→List(X)→αfor some α, where X=α→List(X)→α. Hence weneed some sort of recursive types.The second problem is this: Recall that Cont and Trail are informally definedas Cont =TargetValue →Trail →TargetValue and Trail =List(Cont).When the source language is typed in some way, the type TargetValue shouldbe instantiated by more specific types, and in general, a trail has the type:List(α1→List(α2→List(. . . List(αn→ · · · → βn)...)→β2)→β1)for different αiand βi. Apparently, we cannot represent these types in a finitemanner.We give a simple solution to these problems based on the observation thatmost (if not all) examples with control/prompt in the literature can be typedunder the following simple restriction:7
–In a trail type, all αiand βiis the same type.This means that any trail must have type uX.List(τ→X→τ) for some typeτwhere uis for recursive types. In the sequel, we adopt this restriction, andwrite Trail(τ) for this type. Note that the restriction does not constrain thetype of continuations, that is, a continuation may have type α→Trail(τ)→βfor different types α,β, and τ.We think that this restriction is not too strong, since, most (if not all) exam-ples with control/prompt in the literature follow this restriction (list-reversingfunction and several variations of search programs [6]). Also we will see later thatthe typed control/prompt calculus under this restriction can simulate typedshift/reset calculus, which has many interesting examples.Under this restriction, the target terms of the CPS translation can be typed inthe ordinary type system (with let-polymorphism, but without recursive types),in which the most general type always exists (if typable), and, therefore, the firstproblem is also solved.Discussion. An anonymous reviewer has suggested us that, we could excludethe circularity in the trail types by introducing an inductive (not recursive)structure. One way to achieve it is: if we change the definition of the trail typefrom Trail =List(Cont) toTrail(n) = Trail(0) |(Cont ×Trail(n-1))where ndenotes the length of the list, then we can avoid the circularity (re-cursiveness) of the trail type. However, the use of dependent types drasticallycomplicates the type structure of the target calculus (and possibly the corre-sponding source type system). Moreover, it is not our goal to obtain a stronglynormalizing calculus for control/prompt by constraining the source type systemartificially. Rather, we took Biernacki et al.’s CPS translation as a good startingpoint, and based on it, we tried to construct a natural type system which isharmonious with their CPS translation.4.2 Definition of Type SystemNow we introduce a type system for control/prompt.Types and type contexts are defined by:α, β ··· ::= b|t|α→(β, γ, δ/τ ) monomorphic typesA::= α| ?t.A polymorphic typesΓ::= [ ] |Γ, x :Atype contextswhere bis a basic type (including bool), tis a type variable, and α→(β, γ, δ /τ)is a function type whose meaning will be made clear later. FTV(A) denotes theset of free type variables in A.The type system has two forms of judgements, and the first form is:Γ`e:α, β, γ /τ8
(x:A∈Γand α≤A)Γ`px:αvar (dis constant of type b)Γ`pd:bconstΓ, x :α`e:β, γ, δ /τΓ`pλx.e :α→(β, γ , δ/τ )fun Γ`pe:αΓ`e:α, β, β /τ expΓ`e1:α→(β, γ , δ/τ ), ?, ρ/τ Γ `e2:α, δ, ?/τΓ`e1e2:β, γ , ρ/τ appΓ`e1:bool, δ, γ/τ Γ `e2:α, β, δ/τ Γ `e3:α, β, δ /τΓ`if e1then e2else e3:α, β, γ /τ ifΓ`pe1:ρ Γ, x :Gen(ρ;Γ)`e2:α, β, γ/τΓ`let x=e1in e2:α, β, γ /τ letΓ`e:τ, τ , β/τΓ`p#e:βprompt Γ, c :α→(τ, τ , β/τ )`e:ρ, ρ, γ/ρΓ` Fc.e :α, β, γ/τ controlFig. 5. Type Inference Ruleswhere Γis a type context, α,β,γ, and τare types, and eis an expression. Itmeans that, under the type context Γ,eis an expression of type α, with theanswer type modification2from βto γ, and the trail type is τ. The roles of theadditional types in the judgement can be made clearer by CPS translating it:Γ*`[[e]] : Cont(α*, β */τ*)→Trail(τ*)→γ*withTrail(τ*) = uX.List(τ*→X→τ*)Cont(α*, β*/τ *) = α*→Trail(τ*)→β*The second form of judgements is:Γ`pe:αwhich means eis a pure (effect-free) expression of type α. This form is used tointroduce let-polymorphism with control effects in a sound manner[2].Figure 5 gives the type inference rules where α≤Ain the rule (var) means, ifA≡ ?t1.···?tn.ρ for some monomorphic type ρ, then τ≡ρ[σ1,··· , σn/t1,··· , tn]for some monomorphic types σ1,· · · , σn. We assume that, a basic type bis as-sociated with each constant d. The type Gen(ρ;Γ) in the rule (let) is defined by?t1.· · · ?tn.ρ where {t1,··· , tn}=FTV(ρ)-FTV(Γ).The rule (exp) allows one to switch from the second form to the first form.Since pure expressions are insensitive to continuations and trails, we can intro-duce arbitrary types for their answer type (β) and the trail type (τ).2For the standard CPS translation, we say, the answer type is modified in a compu-tation of efrom βto γ, if the CPS transform of ehas type (α→β)→γ. Withoutcontrol operators for delimited continuations, the types βand γare equal. Withthem, they may be different. See Asai and Kameyama [2] for details.9
Γ`e:α, β, γ /tΓ`e:α, β, γ /*star-intro, if t6∈ FTV(Γ, α, β , γ)Γ`e:α, β, γ /*Γ`e:α, β, γ /τ star-elimΓ`e:α→(β, γ , δ/*), ?, ρ/σΓ`e:α→(β, γ , δ/τ ), ?, ρ/σ star-funFig. 6. Type Inference Rules for λc/p+letOther rules are naturally derived from the type for the CPS translation.The rule (var) is standard. In the rule (fun), the function type α→(β, γ, δ/τ )extends the ordinary function type α→βto encapsulate the effect of answertype modification from γto δwith the trail type τ. The rule (app) reflects thisintuition. The rule (let) is for ML-like let-polymorphism. As is well known, wemust restrict e1in the expression let x=e1in e2to have a sound type system,and we follow Asai and Kameyama’s type system [2] which restricts e1to be apure term, i.e., either a value or # e.For the rule (prompt), look at its CPS translation in Figure 4. It is easy tocheck θ1must have type Cont(τ, τ /τ) for some τ, and the return type of [[e]] is thesame as that of [[# e]]. So by letting this return type β, we get the rule (prompt).The rule (control) is more complicated. In the CPS translation of Fc.e, a termλxk0t0.kx(t@(k0:: t0)) is substituted for c, which poses constraints that tand t0are of the same list type and k0is of its member type. Since we restricted alltrails to be of type Trail(τ) for some τ,k0has to have the type Cont(τ, τ /τ )and tand t0have the type Trail(τ). Then we can derive the rule (control).An example type derivation for a concrete term will be given in a later section.We call the calculus with this type system λc/plet .4.3 Introducing Trail-PolymorphismThe type system of λc/plet can type many useful examples with control/prompt.However, it cannot express a certain kind of polymorphism in trails. We occa-sionally want to express that a function has type α→(β, γ, δ/τ ) for any τ,i.e., it is insensitive (or polymorphic) to the trail type. To solve this problemwith a small cost, i.e., not without introducing impredicative polymorphism, weintroduce a limited form of polymorphism, called trail-polymorphism, into λc/pletas follows.We add a special type constant “*” to the definition of types, which canappear in a function type as α→(β, γ, δ/*), or in a judgement as Γ`e:α, β, γ /*. Intuitively, *represents a universally quantified type variable.We add to λc/plet three new type inference rules listed in Figure 6, which reflectthe intuitive meaning of *. We call the extended calculus λc/p+let . Note that thereductions rules are the same as those for λc/plet .10
We can also introduce impredicative polymorphism in the same manner asthat system for shift/reset[2]. Since it is orthogonal to the present type system,we omit the details in this paper.5 PropertiesIn this section, we state basic properties of λc/plet and λc/p+let . Due to lack of space,we only state proof sketches in this paper.The first property, subject reduction, is by far the most important propertyin a typed calculus.Theorem 1 (Subject Reduction). If Γ`e1:α, β, γ/τ is derived and e1?e2, then Γ`e2:α, β, γ /τ can be derived.The theorem is proved by the standard induction on the derivation. For thecase of the reduction # (P[Fc.e]) ?# (let c=λx.P [x]in e), we decomposeit into several smaller reductions as in [3], then the theorem is easy to prove.The next theorem is the progress property which states the computation ofa well typed, closed expression does not get stuck. Here, the word “close” meansthat the term does not have any free variables and any occurrences of controlwhich are not enclosed by prompt. To ensure the last property, we restrict ourattention to an expression in the form # e. A redex is one of the expressions inthe lefthand sides of the reduction rules in Figure 3.Theorem 2 (Progress). If `#e:α, β , γ/τ is derivable, then #eis in theform E[r]where Eis an evaluation context and ris a redex.Note that, if eis a value v, # eitself is a redex which reduces to v. Theprogress property is proved by the standard case analysis.These two theorems together constitute the strong type soundness property.The next theorem states that our type system is compatible with the CPStranslation. For this purpose, we define the type structure of the target calculusdepending on the source calculus by:–for λc/plet , the target calculus is (predicatively) polymorphic lambda calculuswith conditionals, the trail type Trail(τ), and the list type.–for λc/p+let , the target calculus is impredicatively polymorphic lambda calculus(second order lambda calculus) with conditionals, the trail type Trail(τ),and the list type.We define the CPS translation for types and type contexts by:α*=αfor basic type and type variable(α→(β, γ , δ/τ ))*=α*→(β*→Trail(τ*)→γ*)→Trail(τ*)→δ*(α→(β, γ , δ/*))*=α*→ ?X.((β*→Trail(X)→γ*)→Trail(X)→δ*)[ ]*= [ ](Γ, x :?t1...tn.α)*=Γ*, x :?t1. . . tn.α*11
The third line is for λc/p+let only. We then state type preservation property as atheorem.Theorem 3 (Type Preservation for CPS Transformation).–(For λc/plet and λc/p+let ) If Γ`e:α, β, γ /τ is derivable for τ6=*, then Γ*`[[e]] : (α*→Trail(τ*)→β*)→Trail(τ*)→γ*is derivable in the targetcalculus.–(For λc/p+let ) If Γ`e:α, β, γ /*is derivable, then Γ*`[[e]] : (α*→Trail(τ)→β*)→Trail(τ)→γ*is derivable for any τin the targetcalculus.In this paper, we do not state the property that equality is preserved by CPStranslation, since it is independent to our type system, and in order to state theproperty as a theorem, we need to develop a sophisticated equality theory in thetarget language. For the latter, we need the following property for an arbitrarypure evaluation context P:λx k1t1.[[P[x]]] θ1(k1:: t1) = λx k1t1.[[P[x]]] k1t1which is about the inductive nature of trails (lists). Since t1in this equation isa bound variable, we need to elaborate an inductive theory.6 Encoding Shift/Reset by Control/PromptIn type-free setting, shift/reset can be macro-defined by control/prompt [4],and we show in this section that it also holds for the typed setting here. Weadopt the calculus λs/rlet in [2] for shift/reset, since it is the most liberal typesystem which allows answer-type modification and let-polymorphism. Its typeinference rules are listed in the appendix.We define a translation from λs/rlet to λc/p+let as follows:Types (α/γ →β/δ) = α→(β, γ, δ /*)Expressions Sc.e =Fc0.let c=λx.# (c0x)in ehei= # eType Contexts Γ, x :?t1...tn.α =Γ , x :?t1. . . tn.αFor other constructs, the translation is homomorphic. This translation preservestypes and reduction.Theorem 4.–If Γ;β`e:α;γis derivable in λs/rlet ,Γ`e:α, β, γ /*is derivable in λc/p+let .–If Γ;β`e1:α;γis derivable and e1?e2in λs/rlet ,e1?*e2in λc/p+let .12
Proof. We prove this theorem by induction on the derivation of Γ;β`e:α;γ.We list two key cases here.(Reset) Suppose we have a derivation in λs/rlet :....Γ;α`e:α;βΓ;γ` hei:β;γresetBy induction hypothesis, we can derive Γ`e:α, α, β/*. Then we can derive:Γ`e:α, α, β/*Γ`e:α, α, β/αΓ`p#e:βΓ` hei= # e:β, γ , γ/*(Shift) Suppose we have a derivation in λs/rlet :....Γ, c :?t.(β/t →α/t); δ`e:δ;γΓ;α` Sc.e :β;γshiftLet ?1=Γ , c :?t.(β→(α, t, t/*)). By induction hypothesis, we have a deriva-tion for ?1`e:δ, δ, γ /*in λc/p+let . Let ?2=Γ , c0:β→(s, s, α/s) where sis afresh type variable, then we can derive:?2, x :β`c0x:s, s, α/s?2, x :β`p# (c0x) : α?2, x :β`# (c0x) : α, t, t/*?2`pλx.# (c0x) : β→(α, t, t/*)?2`pλx.# (c0x) : β→(α, t, t/*)?1`e:δ, δ, γ/*?1`e:δ, δ, γ /δ?2`let c=λx.# (c0x)in e:δ, δ, γ /δΓ` Fc0.let c=λx.# (c0x)in e:β, α, γ/sSince s6∈ FTV(Γ , α, β , γ), we can derive Γ` Sc.e :β, α, γ/*.We can also show that, if e?e0in λs/rlet , then e?*e0in λc/p+let , whose keycase is proved as follows:hP[Sc.e]i=#(P[Fc0.let c=λx.#c0xin e])?# (let c0=λy.P [y]in let c=λx.#c0xin e)?# (let c=λy.# (λy.P [x])xin e)?# (let c=λx.#P[x]in e)=hlet c=λx.hP[x]iin eiWe remark that this proof does not work for λc/plet .13
7 Typed Control/Prompt is Strictly More ExpressiveThan Shift/ResetIn the type-free setting, we can encode control/prompt in terms of shift/reset[7, 15, 6]. In the typed setting, it is not the case, as we will prove in this section.Since λs/rlet is strongly normalizing [2], it is sufficient to construct a typable ex-pression in λc/p+let (or λc/plet ) whose computation is not terminating.Let αand o, resp. be a type and its inhabitant, resp., for instance, α=booland o=true. Let Γbe the type context c:α→(α, α, α/α), and recall e1;e2is an abbreviation of (λx.e2)e1for x6∈ FV(e2). We can type the expression# (Fc.(co;co); Fc.(co;co)) in λc/plet as follows:Γ`c:α→(α, α, α/α), α, α/α Γ ` o :αΓ`co:α, α, α/αΓ`co;co:α, α, α/α`pFc.(co;co) : α` Fc.(co;co); Fc.(co;co) : α, α, α/α`# (Fc.(co;co); Fc.(co;co)) : α, β, β /τThe computation of this term does not terminate:# (Fc.(co;co); Fc.(co;co))?# (let c=λu.(u;Fc.(co;co)) in (co;co))?*# (Fc.(co;co); (λu.(u; # Fc.(co;co)))o)?*# (Fc.(co;co); (λu0.(u0; (λu.(u; # Fc.(co;co)))o))o)?*...Since this example does not use answer-type modification or polymorphism, itcan be typed in a more restricted type system such as our previous one [20].We can go a step further. After submission of this paper, Kiselyov [16] andthe second author (Yonezawa) have independently constructed fixed point com-binators in call-by-value:(Kiselyov)Y1=λf.# (Zf;Zf) where Zf=Fc. f (λx. # (co;co)x)(Y onezawa)Y2=λf.# (Xf;Xf) where Xf=Fc. λx. (f# (co;co)) xBoth Y1and Y2are typable in λc/plet , and satisfy Y1f x =f(λx. Y1f x)x, andY2f x =f(λx. f (Y2f)x)x. Therefore, they can serve as fixed point combina-tors. The former satisfies a simpler equation, while Y1emay not terminate forsome term e, but Y2ealways terminates.8 ConclusionWe have introduced a polymorphic type system for control/prompt, which al-lows answer type modification and does not need recursive types. We have shown14
that our calculus enjoys type soundness and is compatible with the CPS trans-lation, and that typed control/prompt is strictly more powerful than typedshift/reset in the absence of recursive types. Although we cannot claim thatour type system is *the* only type system for control/prompt, we believe thatours can be a good starting point to study the type structure of these controloperators.Based on this work, Kiselyov and the second author have successfully shownthat λc/plet is Turing-complete if we extend the calculus with integers and prim-itive functions. The situation is similar to the exception mechanism in ML, forwhich Lillibridge [17] has proved that typed (unchecked) exception can simulateall type-free lambda terms, and therefore can represent all Turing-computablefunctions. Thielecke also compared the expressive powers of several control op-erators using a different technique [19].In this paper we have been concentrating on the foundational aspect ofcontrol/prompt in this paper, and the practical aspect of our type systemsis unstudied. In particular, more application programs other than those by Bier-nacki, Danvy, Millikin’s are called for, but it is left for future work.Acknowledgements: We thank Kenichi Asai, Dariusz Biernacki, OlivierDanvy, and Chung-chieh Shan for their insights. Special thanks go to Oleg Kise-lyov and anonymous reviewers for valuable comments. This work was partlysupported by JSPS Grant-in-Aid for Scientific Research (C) .References1. K. Asai. On Typing Delimited Continuations: Three New Solutions to the PrintfProblem. Technical Report OCHA-IS 07-1, Department of Information Science,Ochanomizu University, September 2007.2. K. Asai and Y. Kameyama. Polymorphic Delimited Continuations. In Proc. AsianProgramming Languages and Systems, LNCS 4807, pages 239–254, Nov-Dec 2007.3. K. Asai and Y. Kameyama. Polymorphic Delimited Continuations. TechnicalReport CS-TR-07-10, Dept. of Computer Science, University of Tsukuba, Sep 2007.4. D. Biernacki and O. Danvy. A Simple Proof of a Folklore Theorem about DelimitedControl. J. Funct. Program., 16(3):269–280, 2006.5. D. Biernacki, O. Danvy, and C. c. Shan. On the Static and Dynamic Extents ofDelimited Continuations. Science of Computer Programming, 60(3):274–297, 2006.6. D. Biernacki, O. Danvy, and K. Millikin. A Dynamic Continuation-Passing Stylefor Dynamic Delimited Continuations. TOPLAS, to appear.7. C. c. Shan. Shift to control. In Proc. Workshop on Scheme and Functional Pro-gramming, pages 99–107, 2004.8. O. Danvy. Functional Unparsing. J. Funct. Program., 8(6):621–625, 1998.9. O. Danvy and A. Filinski. Abstracting Control. In Proc. 1990 ACM Conferenceon Lisp and Functional Programming, pages 151–160, 1990.10. O. Danvy and A. Filinski. Representing Control: a Study of the CPS Transforma-tion. Mathematical Structures in Computer Science, 2(4):361–391, 1992.11. R. K. Dybvig, S. Peyton Jones, and A. Sabry. A Monadic Framework for DelimitedContinuations. J. Funct. Program., to appear.12. M. Felleisen. The Theory and Practice of First-Class Prompts. In Proc. 15thSymposium on Principles of Programming Languages, pages 180–190, 1988.15
13. A. Filinski. Representing Monads. In POPL, pages 446–457, 1994.14. Y. Kameyama and M. Hasegawa. A sound and complete axiomatization for de-limited continuations. In ICFP, pages 177–188, 2003.15. O. Kiselyov. How to remove dynamic prompt: Static and dynamic delimited contin-uation operators are equally expressive. Technical Report 611, Computer ScienceDepartment, Indiana University, March 2005.16. O. Kiselyov. Fixpoint combinator from typed prompt/control. 2007.http://okmij.org/ftp/Computation/Continuations.html.17. M. Lillibridge. Unchecked Exceptions Can Be Strictly More Powerful ThanCall/CC. Higher-Order and Symbolic Computation, 12(1):75–104, 1999.18. C. Strachey and C. P. Wadsworth. Continuations: A mathematical semantics forhandling full jumps. Technical Monograph PRG-11, Oxford Univ. Comput. Lab.,Oxford, England, 1974. Reprinted in Higher-Order and Symbolic Computation13(1/2):135–152, 2000.19. H. Thielecke. On Exceptions Versus Continuations in the Presence of State. InESOP, pages 397–411, 2000.20. T. Yonezawa and Y. Kameyama. A Type System for Dynamic Delimited Contin-uations. IPSJ Transactions on Programming, Information Processing Society ofJapan, to appear.A Polymorphic Type System for shift/resetWe define the type system for λs/rlet in [2] except the fixed point operator. Typesand type contexts are defined by:α, β ··· ::= b|t|(α/β →γ/δ) monomorphic typesA::= α| ?t.A polymorphic typesΓ::= [ ] |Γ, x :Atype contextswhere the function type (α/β →γ/δ) corresponds to α→(γ, β , δ/*) in λc/p+let .Judgements in λs/rlet are either Γ;α`e:β;γor Γ`pe:β. The former corre-sponds to Γ`e:β, α, γ/*in λc/p+let . Finally, Figure 7 gives several importanttype inference rules of λs/rlet .Γ, x :σ;α`e:τ;βΓ`pλx.e : (σ/α →τ /β)funΓ, k :?t.(τ/t →α/t); σ`e:σ;βΓ;α` Sk.e :τ;βshift Γ;σ`e:σ;τΓ`phei:τresetFig. 7. Type Inference Rules of λs/rlet .16
CitationsCitations9ReferencesReferences20Although focusing is orthogonal to the red/green colors of ACL, we shall discuss how ACL can still be focused in Section 8. To facilitate comparison with existing systems for delimited continuations (e.g. [14]), we formalize terms, values and evaluation contexts as follows:
ABSTRACT: This paper modifies our previous work in combining classical logic with intuitionistic logic [16, 17] to also include affine linear logic, resulting in a system we call Affine Control Logic. A propositional system with six binary connectives is defined and given a phase space interpretation. Choosing classical, intuitionistic or affine reasoning is entirely dependent on the subformula property. Moreover, the connectives of these logics can mix without restriction. We give a sound and complete sequent calculus that requires novel proof transformations for cut elimination. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. One of our goals is to allow non-classical restrictions to coexist with computational interpretations of classical logic such as found in the λμ calculus. In fact, we show that the transition between different modes of proof, classical, intuitionistic and affine, can be interpreted by delimited control operators. We also discuss how to extend the definition of focused proofs to this logic.Conference Paper · Jul 2016 · ACM Transactions on Programming Languages and SystemsWe will not go into the details of other variants here, but refer to the literature instead (Dyvbig et al. 2007; Shan 2004; Biernacki et al. 2006); suffice it to note that the two main variants, at least in an untyped setting, are equally expressive and have been shown to be macro-expressible (Felleisen 1991) by each other (Shan 2004; Kiselyov 2005 ). Applying the type systems of Asai and Kameyama (2007); Kameyama and Yonezawa (2008) , however, renders the dynamic control operators strictly more expressive since strong normalization holds only for the static variant (Kameyama and Yonezawa 2008). In Danvy and Filinski's model, there are two primitive operations , shift and reset. ABSTRACT: We describe the implementation of first-class polymorphic delimited continuations in the programming language Scala. We use Scala's pluggable typing architecture to implement a simple type and effect system, which discriminates expressions with control effects from those without and accurately tracks answer type modification incurred by control effects. To tackle the problem of implementing first-class continuations under the adverse conditions brought upon by the Java VM, we employ a selective CPS transform, which is driven entirely by effect-annotated types and leaves pure code in direct style. Benchmarks indicate that this high-level approach performs competitively. Full-text · Article · Aug 2009 ABSTRACT: The notion of delimited continuations has been proved useful in various areas of computer programming such as partial evaluation, mobile computing, and web transaction. In our previous work, we proposed polymorphic calculi with control operators for delimited continuations. This paper presents a proof of strong normal- ization (SN) of these calculi based on a refined (i.e. administrative redex-free) CPS translation. Full-text · Article · ACM Transactions on Programming Languages and SystemsABSTRACT: We study the control operators &control& and &prompt& which manage part of continuations, that is, delimited continuations. They are similar to the well-known control operators &shift& and &reset&, but differ in that the former is dynamic, while the latter is static. In this paper, we introduce a static type system for &control& and &prompt& which does not use recursive types. We design our type system based on the dynamic CPS transformation recently proposed by Biernacki, Danvy and Millikin. We also introduce let-polymorphism into our type system, and show that our type system satisfies several important properties such as strong type soundness.Article · Jan 2008
Full-text · Article · Jan 2008 · ACM Transactions on Programming Languages and Systems+1 more author...ABSTRACT: We put a preexisting definitional abstract machine for dynamic delimited continuations in defunctionalized form, and we present the consequences of this adjustment. We first prove the correctness of the adjusted abstract machine. Because it is in defunctionalized form, we can refunctionalize it into a higher-order evaluation function. This evaluation function, which is compositional, is in continuation+state-passing style and threads a trail of delimited continuations and a meta-continuation. Since this style accounts for dynamic delimited continuations, we refer to it as &dynamic continuation-passing style& and we present the corresponding dynamic CPS transformation. We show that the notion of computation induced by dynamic CPS takes the form of a continuation monad with a recursive answer type. This continuation monad suggests a new simulation of dynamic delimited continuations in terms of static ones. Finally, we present new applications of dynamic delimited continuations, including a meta-circular evaluator. The significance of the present work is that the computational artifacts surrounding dynamic CPS are not independent designs: they are mechanical consequences of having put the definitional abstract machine in defunctionalized form. Full-text · Article · Oct 2015 ArticleJanuary 2008 · IPSJ Digital CourierWe study the control operators &control& and &prompt& which manage part of continuations, that is, delimited continuations. They are similar to the well-known control operators &shift& and &reset&, but differ in that the former is dynamic, while the latter is static. In this paper, we introduce a static type system for &control& and &prompt& which does not use recursive types. We design our... ArticleThe notion of delimited continuations has been proved useful in various areas of computer programming such as partial evaluation, mobile computing, and web transaction. In our previous work, we proposed polymorphic calculi with control operators for delimited continuations. This paper presents a proof of strong normal- ization (SN) of these calculi based on a refined (i.e. administrative... ArticleIn our previous work we gave a sound and complete axioma- tization of the control operators for delimited continuations, shift and reset by Danvy and Filinski and their variants. Since the calculus allows only one use of shift and reset, a next step is to investigate the calculus with many dierent shift's and reset's. In this work, we study the calculus with higher-level delimited continuation... ArticleNovember 2007This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the explicit presence of answer types, our type system satisfies various important properties, including strong type soundness, existence of... Data provided are for informational purposes only. Although carefully collected, accuracy cannot be guaranteed. Publisher conditions are provided by RoMEO. Differing provisions from the publisher's actual policy or licence agreement may be applicable.This publication is from a journal that may support self archiving.Last Updated: 06 Sep 17}