CPS conversion

CPS conversion is the process of translating a TODO calculus into a TODO (CPS) one. This tutorial describes one way of formalizing CPS conversion in STELF. It is an advanced tutorial because it relies on techniques described in other tutorials, such as TODO.

We will define a direct style lambda calculus and its static semantics, then a CPS language and its static semantics. We will then prove that any well-formed direct style expression can be translated into a well-formed CPS expression.

Direct style language

We begin with a direct style lambda calculus with products, unit, and a let construct.

%sort typ %.
%name typ %.
%term => %pi typ %-> typ %-> typ %.
%prec %right 8 => %.
%term & %pi typ %-> typ %-> typ %.
%prec %none 9 & %.
%term unit typ %.
%% expressions
%sort exp %.
%sort val %.
%% values are expressions, too.
%term value %pi val %-> exp %.
%term lam %pi (%pi val %-> exp) %-> val %.
%term app %pi exp %-> exp %-> exp %.
%term mkpair %pi exp %-> exp %-> exp %.
%term pair %pi val %-> val %-> val %.
%term fst %pi exp %-> exp %.
%term snd %pi exp %-> exp %.
%term 1 val %.
%term let %pi exp %-> (%pi val %-> exp) %-> exp %.

Here we make a syntactic distinction between values (of LF type val) and expressions (exp). A constructor value injects syntactic values into expressions. It would also be possible to do a more extrinsic encoding of values by instead defining a judgment over expressions that defined the subset that are values. This encoding makes more facts explicit in the typing (for instance it is immediately evident that the calculus is call-by-value since lambdas expect values as arguments) which resists mistakes and saves us some lemmas. Note that we distinguish between the expression mkpair whose evaluation creates a pair and the value that results, pair.

The typing rules for this language are straightforward:

% |- e : t
%sort of {_ exp} {_ typ} %.
% |- v : t
%sort ofv {_ val} {_ typ} %.
%term ofvalue %pi (of (value V) A) %<- (ofv V A) %.
%term unitI ofv 1 unit %.
%term =>I
  %pi (ofv (lam ([x val] M x)) (A => B))
  %<- ({x val} %pi (ofv x A) %-> (of (M x) B)) %.
%term =>E %pi (of M1 (A => B)) %-> (of M2 A) %-> (of (app M1 M2) B) %.
%term &Iv %pi (ofv V1 A) %-> (ofv V2 B) %-> (ofv (pair V1 V2) (A & B)) %.
%term &I %pi (of M1 A) %-> (of M2 B) %-> (of (mkpair M1 M2) (A & B)) %.
%term &E1 %pi (of (fst M) A) %<- (of M (A & B)) %.
%term &E2 %pi (of (snd M) B) %<- (of M (A & B)) %.
%term oflet %pi (of M A) %-> ({y val} {ofy ofv y A} of (N y) C) %-> (of (let M N) C) %.

The type family of M A encodes the typing judgment $\\Gamma \\vdash M : A$, and ofv V A the judgment $\\Gamma \\vdash V : A$.

CPS language

We then define the syntax of the CPS language that will be the target of CPS conversion:

%% CPS language
%sort cexp %.
%name cexp %.
%sort ctyp %.
%name ctyp %.
%sort cval %.
%name cval %.
%term ccont %pi ctyp %-> ctyp %.
%prec %postfix 8 ccont %.
%term c& %pi ctyp %-> ctyp %-> ctyp %.
%prec %none 9 c& %.
%term cunit ctyp %.
% continuation expressions
%term cmkpair %pi cval %-> cval %-> (%pi cval %-> cexp) %-> cexp %.
%term cfst %pi cval %-> (%pi cval %-> cexp) %-> cexp %.
%term csnd %pi cval %-> (%pi cval %-> cexp) %-> cexp %.
% continuations can end with a call to a function
%term ccall %pi cval %-> cval %-> cexp %.
%term chalt cexp %.
% continuation values
%term cpair %pi cval %-> cval %-> cval %.
%term clam %pi (%pi cval %-> cexp) %-> cval %.
%term c1 cval %.

This language makes the same syntactic distinction between continuation expressions (cexp) and values (cval). A continuation expression is a linear sequence of operations on values (here cmkpair, cfst and csnd), each of which binds a variable. A continuation expression ends with a call to a continuation (ccall) or by halting (chalt). A continuation value is either a pair of values (cpair), the unit element (c1) or a lambda (clam) which abstracts a continuation expression. Because continuations never return, lambdas have type A ccont for some argument type A. (Note that the ccont type constructor is written in postfix notation.) In some presentations of CPS, this is written as A → 0, A → ⊥, or ¬A.

The static semantics for the CPS language is as follows:

% |- c ok
%sort cof {_ cexp} %.
%name cof %.
%mode cof %star %.
% |- cv : A
%sort cofv {_ cval} {_ ctyp} %.
%name cofv %.
%mode cofv %star %star %.
%term co_halt cof chalt %.
%term co_mkpair
  %pi (cofv V1 A)
  %-> (cofv V2 B)
  %-> ({v cval} %pi (cofv v (A c& B)) %-> (cof (K v)))
  %-> (cof (cmkpair V1 V2 K)) %.
%term co_call %pi (cofv F (A ccont)) %-> (cofv V A) %-> (cof (ccall F V)) %.
%term co_fst %pi (cofv V (A c& B)) %-> ({v} {ov cofv v A} cof (C v)) %-> (cof (cfst V C)) %.
%term co_snd %pi (cofv V (A c& B)) %-> ({v} {ov cofv v B} cof (C v)) %-> (cof (csnd V C)) %.
%term cov_unit cofv c1 cunit %.
%term cov_pair %pi (cofv V1 A) %-> (cofv V2 B) %-> (cofv (cpair V1 V2) (A c& B)) %.
%term cov_lam %pi ({x} %pi (cofv x A) %-> (cof (C x))) %-> (cofv (clam C) (A ccont)) %.

The type family cof C encodes the typing judgment $\Gamma \vdash C\, \mathit{ok}$ . Continuations do not return, so they do not have a type. The type family ofv V A the judgment $\Gamma \vdash C : A$ for CPS values V. The typing rules are straightforward.

Translation

Type translation

We can now translate from the direct style language to the CPS language. Because a translated value will have a different type in the source and destination languages (indeed, the source and destination types are different LF types!), we start by defining a translation for the types of the source language.

%sort ttoct {_ typ} {_ ctyp} %.
%mode ttoct %in %out %.
%term ttoct/unit ttoct unit cunit %.
%term ttoct/& %pi (ttoct (A & B) (A' c& B')) %<- (ttoct B B') %<- (ttoct A A') %.
%term ttoct/=> %pi (ttoct (A => B) (A' c& (B' ccont) ccont)) %<- (ttoct B B') %<- (ttoct A A') %.

The family ttoct A A' (“typ to ctyp”) encodes the type translation, which is often written using Scott brackets $\llbracket A \rrbracket$. The unit type and product types simply translate recursively into their correspondents in the CPS types. An arrow type A → B translates into (A' c& (B' ccont)) ccont. That is, a function is translated into a continuation that expects the (translated) argument paired with a return continuation for the (translated) result.

To check our work, we can verify that type translation is total. This result will not be important to our main theorem, but every type should certainly have a translation and it is an easy way to check for mistakes early.

%worlds () (ttoct _ _) %.
%total D (ttoct D _) %.

Translation relation

The translation for values is a three place relation:

%sort tocpsv+ {WV ofv V A} {CT ttoct A CA} {WCV cofv CV CA} %.
%mode tocpsv+ %in %in %out %.

WV is a value typing derivation in the source language. Our translation will be type-directed, translating typing derivations to typing derivations. The terms, which are in the types of the typing derivations, can easily be recovered (in fact, they are implicit parameters in this judgment). The middle place in the relation is the translation of the type; this is necessary to ensure that the translated value has the appropriate translated type.

Sometimes it is necessary for the type translation to be an output of the relation, and sometimes it is necessary for it to be an input. As is standard for translations between languages, we will need to use the TODO technique to give two versions of this relation with two different modes. The second one is identical except for the mode of the middle argument:

%sort tocpsv- {WV ofv V A} {CT ttoct A CA} {WCV cofv CV CA} %.
%mode tocpsv- %in %out %out %.

The CPS translation relation for expressions, which is the crux of this tutorial, is much less straightforward:

%sort tocps- {M exp} {WM of M A} {CT ttoct A CA} {CC %pi (%pi cval %-> cexp) %-> cexp} {WCC {C %pi cval %-> cexp} %pi ({cv cval} {wcv cofv cv CA} cof (C cv)) %-> (cof (CC C))} %.
%mode tocps- %in %in %out %out %out %.

For this relation we will use explicit parameters for the terms. The first two arguments are the expression M to be translated and its typing WM (the letter w is often used in variable names within this code to stand for “well-formed”). The next argument is the translation for the type A of the expression, as in the translation for values. The argument CC is the continuation expression that is the result of CPS conversion. However, it is parameterized over the “tail” of the continuation (of type cval ->; cexp), because an expression cannot be CPS-converted in isolation. For example, the direct style expression mkpair 1 1 will translate into

[rest : cval -> cexp]
  cmkpair c1 c1 [p : cval]
  rest p

The output CC is accompanied by WCC, a typing derivation for it. The typing derivation is also parameterized. Its type is

{C : cval -> cexp}
({cv : cval} {wcv : cofv cv CA} cof (C cv)) ->
 cof (CC C)

The first parameter C is the tail of the continuation, as above. The second argument is a typing derivation for the tail. The tail must be well-formed for any well-formed cval we might pass to it, so that typing derivation is itself parameterized. To summarize, WCC is a parameterized typing derivation that allows us to instantiate it with any well-formed tail.

We also need to give a version of this relation with reversed polarity.

%sort tocps+ {M exp} {WM of M A} {CT ttoct A CA} {CC %pi (%pi cval %-> cexp) %-> cexp} {WCC {C %pi cval %-> cexp} %pi ({cv cval} {wcv cofv cv CA} cof (C cv)) %-> (cof (CC C))} %.
%mode tocps+ %in %in %in %out %out %.

The type of this relation may be more clear when we see how it is used. But before we are able to give the translation for expressions and values, we need to prove some lemmas about the type translation relation.

Lemmas

First, we define a shallow equality relation on continuation types and prove that it is preserved when type constructors are applied:

%sort ceqtyp {_ ctyp} {_ ctyp} %.
%term ceqtyp_ ceqtyp A A %.
%sort ceqtyp_& {_ ceqtyp A A'} {_ ceqtyp B B'} {_ ceqtyp (A c& B) (A' c& B')} %.
%mode ceqtyp_& %in %in %out %.
%term _ ceqtyp_& ceqtyp_ ceqtyp_ ceqtyp_ %.
%sort ceqtyp_cont {_ ceqtyp A A'} {_ ceqtyp (A ccont) (A' ccont)} %.
%mode ceqtyp_cont %in %out %.
%term _ ceqtyp_cont ceqtyp_ ceqtyp_ %.

We need to prove that continuation value typing respects equality, and that continuation tail typing respects equality. These theorems are trivial because equality is shallow.

%sort cofv_resp {_ cofv C A} {_ ceqtyp A A'} {_ cofv C A'} %.
%mode cofv_resp %in %in %out %.
%term _ cofv_resp D ceqtyp_ D %.
%sort wcc_resp {WCC {C %pi cval %-> cexp} %pi ({cv cval} {wcv cofv cv A} cof (C cv)) %-> (cof (CC C))} {EQ ceqtyp A A'} {K' {C %pi cval %-> cexp} %pi ({cv cval} {wcv cofv cv A'} cof (C cv)) %-> (cof (CC C))} %.
%mode wcc_resp %in %in %out %.
%term wcc_resp_ wcc_resp D ceqtyp_ D %.

It is also necessary that the type translation relation ttoct be a function. That means we must prove a uniqueness lemma and effectiveness lemma for it.

% uniqueness
%sort ttoct_fun {_ ttoct A A'} {_ ttoct A A''} {_ ceqtyp A' A''} %.
%mode ttoct_fun %in %in %out %.
%term _
  %pi (ttoct_fun (ttoct/& A B) (ttoct/& C D) OUT)
  %<- (ttoct_fun A C EQ1)
  %<- (ttoct_fun B D EQ2)
  %<- (ceqtyp_& EQ1 EQ2 OUT) %.
%term _
  %pi (ttoct_fun (ttoct/=> A B) (ttoct/=> C D) OUT)
  %<- (ttoct_fun A C EQ1)
  %<- (ttoct_fun B D EQ2)
  %<- (ceqtyp_cont EQ2 EQ3)
  %<- (ceqtyp_& EQ1 EQ3 EQ4)
  %<- (ceqtyp_cont EQ4 OUT) %.
%term _ ttoct_fun ttoct/unit ttoct/unit ceqtyp_ %.
% effectiveness
%sort ttoct_gimme {A typ} {A' ctyp} {_ ttoct A A'} %.
%mode ttoct_gimme %in %out %out %.
%term _
  %pi (ttoct_gimme (A & B) _ (ttoct/& CT1 CT2))
  %<- (ttoct_gimme A A' CT1)
  %<- (ttoct_gimme B B' CT2) %.
%term _
  %pi (ttoct_gimme (A => B) _ (ttoct/=> CT1 CT2))
  %<- (ttoct_gimme A A' CT1)
  %<- (ttoct_gimme B B' CT2) %.
%term _ ttoct_gimme unit cunit ttoct/unit %.

We can then check that these are total:

%worlds () (ttoct_fun _ _ _) (ceqtyp_& _ _ _) (ceqtyp_cont _ _) %.
%total D (ceqtyp_& D _ _) %.
%total D (ceqtyp_cont D _) %.
%total D (ttoct_fun D _ _) %.

Term translation

We can now give the translation for expressions and values. We start by proving the tocpsv+ and tocps+ lemmas, since they are one case each:

%term tocps+/-
  %pi (tocps+ V WV CTi CC K)
  %<- (tocps- V WV CTo CC K')
  %<- (ttoct_fun CTo CTi EQ)
  %<- (wcc_resp K' EQ K) %.
%term tocpsv+/-
  %pi (tocpsv+ WV CTi WCV')
  %<- (tocpsv- WV CTo WCV)
  %<- (ttoct_fun CTo CTi EQ)
  %<- (cofv_resp WCV EQ WCV') %.

Both work the same way. We take the type translation as input (CTi), then invoke the version of the theorem that returns it as output (CTo). Suppose CTi : ttoct A A' and CTo : ttoct A A''. We just need to show that the output of that theorem (K or WCV), which depends on A'', works for the type A'. We simply verify that A' and A'' are equal with our lemma ttoct_fun, and then use the fact that the outputs respect equality on types (wcc_resp or cofv_resp) to do so.

The translation of the expressions fst and snd are illustrative:

%term c_fst
  %pi (tocps- (fst M) (&E1 WM) CT ([tail %pi cval %-> cexp] CC ([v cval] cfst v ([a cval] tail a))) ([c] [wc] F _ ([v] [wv] co_fst wv wc)))
  %<- (tocps- M WM (ttoct/& CT _) CC F) %.
%term c_snd
  %pi (tocps- (snd M) (&E2 WM) CT _ ([c] [wc] F _ ([v] [wv] co_snd wv wc)))
  %<- (tocps- M WM (ttoct/& _ CT) _ F) %.

To translate the expression fst M, we inductively translate the argument. It must have type A & B and so the only case for translating it is ttoct/&, so this subgoal covers all outputs. We return the translation for A, called CT. We must then build the continuation expression and its typing derivation. The expression is parameterized by a tail that takes the result of the fst operation, so the tail has type cval ->; cexp. The resulting term first evaluates M by invoking its translation CC on a tail we write; that tail takes v, the pair value, performs cfst on it and binds the result to a. It finishes by invoking the outer tail argument on that projected first component.

The parameterized typing derivation is similar. It takes a tail c and a typing derivation for the tail, wc. The derivation starts with the typing for the translation of M, which is represented by the function F. We apply F to the actual tail we produce—STELF can deduce what this is by unification, so we just write _ to avoid repeating ourselves. The second argument is the typing derivation for that tail; it takes a variable v representing the result of evaluating M and a typing derivation for it wv. The derivation consists simply of the typing rule for c_fst applied to the well-formedness of its argument and the code that follows, both of which we get from arguments.

The translation is challenging because it is so high-order (typing responsibilities pass from callee to caller and vice versa) but most of the cases follow the same pattern. The case for c_snd is symmetric, but we have now left out terms that STELF can infer by type inference and unification. Because terms can be uniquely determined from the types of typing derivations, we almost never need to write them down explicitly.

The translation for mkpair follows the same pattern.

%term c_mkpair
  %pi (tocps- (mkpair M1 M2) (&I WM1 WM2) (ttoct/& CT1 CT2) _ ([c] [wc] F1 _ ([v1] [wv1] F2 _ ([v2] [wv2] co_mkpair wv1 wv2 wc))))
  %<- (tocps- M1 WM1 CT1 _ F1)
  %<- (tocps- M2 WM2 CT2 _ F2) %.

We translate the two subexpressions, string together the continuation expressions that evaluate them, build the pair and pass it to the tail. Application is interesting because of the way functions are represented:

%term c_app
  %pi (tocps- (app M N) (=>E WM WN) CTB _ ([c] [wc] FM _ ([f] [wf] FN _ ([a] [wa] co_mkpair wa (cov_lam ([r] [wr] wc r wr)) ([p] [wp] co_call wf wp)))))
  %<- (ttoct_gimme (A => B) (A' c& (B' ccont) ccont) (ttoct/=> CTA CTB))
  %<- (tocps+ M WM (ttoct/=> CTA CTB) _ FM)
  %<- (tocps+ N WN CTA _ FN) %.

The first subgoal (ttoct_gimme) exists to reconcile the various type translations that will occur: We will have a translation for A, B, and A => B which all must agree. We therefore invoke the effectiveness lemma on the largest type (A => B) and the others will be subterms. We then invoke tocps inductively to translate the function and argument expressions (we use the + version here so that we need not do equality reasoning about the type translations). The resulting typing derivation begins with the derivations for the translation of M and N. Given these, it builds a pair of the argument wa and return continuation. The body of the return continuation is the outermost tail passed to the translation of the app. We then end with a call to the translated function value on the pair we created.

Binding

So far, everything in the source object language has been first order. We’ll now translate the let construct, which is a simple binder.

%term c_let
  %pi (tocps- (let M N) (oflet WM WN) CTN _ ([c] [wc] FM _ ([v] [wv] FN v wv c wc)))
  %<- (ttoct_gimme A A' CTM)
  %<- (tocps+ M WM CTM _ FM)
  %<- ({x} {xof ofv x A} {x'} {x'of cofv x' A'} {thm tocpsv- xof CTM x'of} tocps- (N x) (WN x xof) CTN (CC x') (FN x' x'of)) %.

This translation begins as before, by translating M. We then want to translate the body, N, but it has type val -> exp, so it must be in a subgoal with a hypothetical value variable in context. The subgoal actually introduces five hypotheses: the direct style value x; a derivation that it is well-formed at type A, xof; the CPS value it will be translated to, x'; its derivation x'of; and the case of the theorem that relates the two. Once we have translated N and WN in this context, we build the result typing derivation. Because we have set up the translation such that the tail always takes a value as an argument, we do not need a CPS-level let construct; we simply invoke FM, which types the translation of M, and then invoke FN on the value and typing derivation resulting from that, and continue with the outermost tail.

The final case of translation for expressions is the inclusion of values:

%term c_val
  %pi (tocps- (value V) (ofvalue WV) CT _ ([c] [wc] wc CV WCV))
  %<- (tocpsv- WV CT WCV) %.

It simply invokes the mutually inductive translation tocpsv-, which we define next.

Value translation

Value translation is not continuation-based, so two of the three cases are very easy:

%term cv_pair
  %pi (tocpsv- (&Iv WV1 WV2) (ttoct/& CT1 CT2) (cov_pair WV1' WV2'))
  %<- (tocpsv- WV1 CT1 WV1')
  %<- (tocpsv- WV2 CT2 WV2') %.
%term cv_unit tocpsv- unitI ttoct/unit cov_unit %.

Pairs are translated pointwise and unit is trivial.

The final case in the theorem is the translation of lambda values:

%term cv_lam
  %pi (tocpsv- (%the (ofv (lam M) (A => B)) (=>I WM)) (ttoct/=> CTA CTB) (cov_lam ([arg] [argof cofv arg (A' c& (B' ccont))] co_fst argof ([x cval] [xof cofv x A'] co_snd argof ([r cval] [rof cofv r (B' ccont)] F x xof r rof ([v cval] ccall r v) ([v cval] [wv cofv v B'] co_call rof wv))))))
  %<- (ttoct_gimme A A' CTA)
  %<- ({x} {xof ofv x A} {x'} {x'of cofv x' A'} {thm tocpsv- xof CTA x'of} {r} {rof cofv r (B' ccont)} tocps- (M x) (WM x xof) CTB (CC x' r) (F x' x'of r rof)) %.

Recall that the tocpsv relations are between typing derivations only (the terms are implicit) but tocps takes them explicitly. Thus the first thing to notice is that we use type annotations to recover the implicit arguments so that we can pass them explicitly to tocps. (This is an instance of converting between implicit and explicit parameters.) As before, we then use effectiveness to translate the type A. The inductive call to tocps has seven hypotheses. The first five are as in the case for let, which represent the bound argument variable and its translation. The last two represent the return continuation, which will be another argument to the continuation we generate. Also notice that in this case we do not have a wildcard _ for the translated term in the subgoal—we write (CC x' r)—without this help STELF’s higher-order unification cannot resolve all of the constraints. (This one case is the reason that the terms cannot be implicit parameters as they are for the value translation.) The result of translation is a typing derivation for a continuation. The continuation’s argument arg has type (A' c& (B' ccont)); we start by projecting the first and second components of the pair. We then use the derivation for the translated body, which depends on the argument and return continuation. Its tail takes the result of the body, v and calls the continuation on that value.

Metatheorem

We can now check our metatheorem, which is that these translations are total. We start by declaring blocks for use in the %worlds declarations:

%block blockcvar [A typ] [A' ctyp] [CTA ttoct A A'] {x} {xof ofv x A} {x'} {x'of cofv x' A'} {thm tocpsv- xof CTA x'of}%.
%block blockwcv [CA ctyp] {r} {rof cofv r CA}%.

The first block corresponds to the five hypotheses we needed in the let and lam cases. The second is for the return continuation we assume in the lam case—it does not correspond to any direct style assumption so it need only be well-formed.

For this proof to check we must also make world declarations for the type families cof, cofv, cval and cexp. I believe this has to do with STELF’s overconservativity of world subsumption on third-order metatheorems, but I am not sure of the exact cause. Although they are strange (and meaningless, since we do not check the totality of these type families, whose modes are all *), they pose no problem here:

%block blockcv {v cval}%.
%worlds (blockcv) (cval) (cexp) %.
%worlds (blockwcv) (cofv _ _) (cof _) %.

Then, the world declarations for our theorems and lemmas:

%worlds (blockcvar blockwcv) (tocps+ _ _ _ _ _) (tocps- _ _ _ _ _) (tocpsv+ _ _ _) (tocpsv- _ _ _) (cofv_resp _ _ _) (ttoct_gimme _ _ _) (wcc_resp _ _ _) %.

We can check the lemmas individually for totality; they are simple inductions:

%total A (cofv_resp _ A _) %.
%total A (wcc_resp _ A _) %.
%total A (ttoct_gimme A _ _) %.

Finally, we can check the type-directed translations for totality:

%total (A B C D) (tocpsv- A _ _) (tocpsv+ B _ _) (tocps- _ C _ _ _) (tocps+ _ D _ _ _) %.