Compiling Purely Functional Structured Programs

TL;DR

This paper introduces a language that combines functional and structured imperative programming within pure lambda calculus, implemented via a monadic DSL that produces lambda terms in continuation-passing style.

Contribution

It presents a novel approach to embed structured imperative features into pure lambda calculus using a monadic DSL, bridging functional and imperative paradigms.

Findings

Successfully embeds structured imperative programming in pure lambda calculus.

Implements core language features in a monadic DSL.

Generates lambda terms in continuation-passing style.

Abstract

We present a marriage of functional and structured imperative programming that embeds in pure lambda calculus. We describe how we implement the core of this language in a monadic DSL which is structurally equivalent to our intended source language and which, when evaluated, generates pure lambda terms in continuation-passing-style.

Equations

$$\lambda k.gy(\lambda r.fx(\lambda r^{\prime }.r^{\prime }rk))$$

$$\lambda k.fx(\lambda r.gy(\lambda r^{\prime }.r{r}^{\prime }k))$$

$$\lambda k.gy(\lambda r.fx(\lambda r^{\prime }.r^{\prime }rk))$$

$$(r,\lambda k.gy(\lambda r....))$$

$$(\lambda k.\varphi (kxy))(\lambda xy....)$$

$$\text{fix}(\lambda loopxy.\varphi (loopxy)).$$

$$\lambda ik.k(\lambda j{k}^{\prime }.$$

$$k^{\prime }j$$

$$else:$$

$$fix(\lambda loopab.$$

$$ifb\ne 0:$$

$$ifa>b:$$

$$loop(a-b)b$$

$$else:$$

$$loopa(b-a)$$

$$else{k}^{\prime }a)ij)$$

Full text

1 Pure Functional Programming

One of the frequently touted benefits of being purely functional lies in the ease with which one can reason about programs. Pure functions have predictable and deterministic behaviour. Applying the same pure function to the same argument always yields the same result anywhere in code, thus allowing us to reason equationally about a program.

But the lack of global variables and mutable state might be an impractical restriction for general purpose programming on conventional operating systems, and so it might be argued that it should be targeted to specific domains, such as the system configuration language Nix NixOS , where reproducibility of system builds is highly prized.

Our own ProofScript ProofScript language is a new entry into the pure functional programming space, where the chosen domain is the development of large scale mechanical verifications of mathematics and software. Our model here is based on massive user collaboration, with users working within what is effectively a single development environment.

In this environment, every mechanically verified theorem must be a piece of reproducible, immutable data, much like a Nix derivation. And so in our programming language, in which we write the code that produces the verified theorems, we seek the same discipline of pure functional programming.

2 Structured Programming

Pure functional programming typically emphasises recursion and higher order functions for expressing complex control flow, and this level of abstraction can be intimidating to those coming from imperative backgrounds and more mainstream languages such as Python. However, the common imperative idioms from structured programming are not anathema to the aims of pure functional code. Indeed, the popularity of Static Single Assignment SSA (SSA) in compiler architectures shows that modelling imperative structured programming in a pure representation is of benefit when it comes to performing reliable optimisations and static analyses of code.

ProofScript aims for the best of both worlds, marrying structured programming with a rich functional language whilst maintaining purity. We believe that our language bears a close affinity to the control flow model assumed in SSA, but with additional support for first-class functions and mutual recursion.

Syntactically, basic ProofScript is a language with support for lexical scope, looping and assignment, but with the following key restrictions:

we do not support mutable cells as values; 2. 2.

closures close over the values of variables, not their locations; 3. 3.

function bodies can only assign to variables whose lexical scope is contained in the function body.

Rule 1 should not need additional explanation. Being able to create and pass around mutable storage locations means that the language encodes shared mutable state that can cross arbitrary regions of code.

Rule 2 rules out situations such as:

\KV@do

,commandchars=

{},,

val x = 0  def get () = x  val a = get ()  x = x + 1  val b = get ()  assert (a == b)

Here, we have lost the referential transparency of the expression get (). The meaning of the function was changed by an imperative update.

Rule 3 rules out common idioms from the world of impure functional programming such as the imperative (or object-oriented) counter:

\KV@do

,commandchars=

{},,

val counter =    do      val i = 0      def get () = i      def incr () = i = i + 1      [get, incr]

Assignments, therefore, are not expected to interact much with function definitions, but instead with imperative control flow such as while and for loops, and conditional statements.

3 CPS

Before SSA, there was CPS, or Continuation Passing Style. In this style, we write lambda terms where evaluation order has been completely disambiguated so that any remaining side-effects (such as non-termination) have an explicit ordering.

In CPS, every function takes a future dependent on the function’s result. The future, or continuation, receives this result and outputs the rest of the program, again via continuation-passing style. For a simple example, consider an ambiguous application $f\ x\ (g\ y)$ where all values are atomic. This might be rendered in CPS form by two different lambda terms

[TABLE]

or

[TABLE]

depending on whether we evaluate the outer application right-to-left or left-to-right.

Compilation of functional programs via CPS transformation was the basis for the classic text Compiling with Continuations CC , but the approach has notoriously fallen out of favour. Compiler toolchains such as LLVM LLVM favour SSA, while other popular representations within the functional programming community are the A-normal form ANF , or Moggi’s monadic denotation Monads .

But there have been robust defences CCExt made for CPS in modern times and our own decision to follow the CPS approach was based on an early commitment to free ProofScript from stack overflow and to allow for the later testing of control flow constructs that may benefit from a stackless runtime.

4 CPS Generation

The traditional means of producing CPS is by a transformation from one lambda term to another, but we get straight to it: our CPS terms are generated directly from a monadic combinator language, whose types bear a clear resemblence to the encoding of effects via monads, with the addition of a call-with-current-continuation primitive.

A motivating observation is that we can represent a partially evaluated CPS program by our current continuation together with the name of the last returned value. Thus, in the CPS term

[TABLE]

we could represent the situation just after evaluating $g\ y$ by a pair whose first component is the bound variable representing the input to the current continuation, and whose second component is a lambda term with a hole for that same continuation:

[TABLE]

The hole indicates where the computation continues, while the variable $r$ names the value of the computation thus far.

4.1 Lambda terms

The actual lambda calculus we use for representing ProofScript code, missing only the ability to define functions by mutual recursion, can be given by the datatype:

\KV@do

,commandchars=

{},,

\PY{k+kr}{data} \PY{k+kt}{Var} \PY{n}{a} \PY{o+ow}{=} \PY{k+kt}{Z}             \PY{o}{|} \PY{k+kt}{S} \PY{n}{a}  \PY{k+kr}{data} \PY{k+kt}{Term} \PY{n}{t} \PY{n}{a} \PY{o+ow}{=} \PY{k+kt}{V} \PY{n}{a}                \PY{o}{|} \PY{k+kt}{App} \PY{p}{(}\PY{k+kt}{Term} \PY{n}{t} \PY{n}{a}\PY{p}{)} \PY{p}{(}\PY{k+kt}{Term} \PY{n}{t} \PY{n}{a}\PY{p}{)}                \PY{o}{|} \PY{k+kt}{Abs} \PY{p}{(}\PY{k+kt}{Term} \PY{n}{t} \PY{p}{(}\PY{k+kt}{Var} \PY{n}{a}\PY{p}{)}\PY{p}{)}                \PY{o}{|} \PY{k+kt}{Fix} \PY{p}{(}\PY{k+kt}{Term} \PY{n}{t} \PY{p}{(}\PY{k+kt}{Var} \PY{n}{a}\PY{p}{)}\PY{p}{)}                \PY{o}{|} \PY{k+kt}{Prim} \PY{p}{(}\PY{n}{t} \PY{p}{(}\PY{k+kt}{Term} \PY{n}{t} \PY{n}{a}\PY{p}{)}\PY{p}{)}

That is, a term is either:

• •

a free variable drawn from the alphabet of frees a

• •

an application

• •

an abstraction

• •

a fixpoint of an abstraction

• •

some primitive structure t over terms.

For bound variables, we have used a trick due to Bird and Paterson DeBruijnNested , where we use DeBruijn indices in a typesafe way. Abstractions bind over the first DeBruijn index Z, with outer variables appearing as successors S. This basic idea has recently been used to implement the Ermine compiler Ermine , and the inherent type safety it affords should alleviate concerns about inadvertent variable capture arising during CPS generation.

4.2 CPS primitives

Our CPS type is to be a monad whose values mimic computation in our imperative source language. Thus, while values in this type cumulatively assemble a lambda term in CPS form, they also carry around an environment of variables that are in scope in the source language.

There is also some book-keeping. CPS transformation introduces a lot of new bound variables for continuations and intermediate values, and we want these to be hidden from the user of our CPS type. Thus, we introduce a type

\KV@do

,commandchars=

{},,

\PY{k+kr}{data} \PY{k+kt}{Val} \PY{o+ow}{=} \PY{k+kt}{Inter} \PY{k+kt}{Int} \PY{o}{|} \PY{k+kt}{Free} \PY{k+kt}{String} consisting of indexed intermediate variables generated by CPS by an internal counter and hidden from the user, as well as string variables that the user can generate for themselves:

\KV@do

,commandchars=

{},,

\PY{n}{nextIndex} \PY{o+ow}{::} \PY{k+kt}{CPS} \PY{k+kt}{Int}  \PY{n}{free} \PY{o+ow}{::} \PY{k+kt}{String} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val}

During CPS, we can emit more of the CPS’d term generated so far via the functions:

\KV@do

,commandchars=

{},,

\PY{n}{nest} \PY{o+ow}{::} \PY{p}{(}\PY{k+kt}{Term} \PY{k+kt}{Exit} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{Term} \PY{k+kt}{Exit} \PY{k+kt}{Val}\PY{p}{)}          \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{n+nb}{()}  \PY{n}{end} \PY{o+ow}{::} \PY{k+kt}{Term} \PY{k+kt}{Exit} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Void}

The function nest builds more computation, while end terminates computation, commiting a final and definitive lambda term as the result. As such, the use of the uninhabited type Void indicates that the computation has no possible return value.

Values of type CPS Val, on the other hand, indicate that the computation represents an expression. This refers to the situation described in the previous section: we are holding onto a pair consisting of a lambda term with a hole together with a free variable or the innermost intermediate value bound in a continuation.

5 Pure Structured Programming

The building blocks for writing our pure structured programs can be likened to nodes in the control flow graph of an SSA program. In SSA, assignments within a node are translated to bindings of a right-hand side to a fresh variable. Thus, code such as

\KV@do

,commandchars=

{},,

val x = 0  x = x + 1  x = x + 1 might become

\KV@do

,commandchars=

{},,

val x = 0  val x1 = x + 1  val x2 = x1 + 1

The variable corresponding to the final assignment to x, namely x2, is then exported from the node in the control flow graph and may be imported into successor nodes by a special function $\phi$.

In our CPS version, the successor nodes are continuations. Assignments are still translated to rebindings, but the values after the final assignments are thrown as extra arguments to these continuations.

Our CPS language structures programs into blocks, similar to nodes in a control flow graph. A block is a function from a CPS computation to another CPS computation. The block computes the set of possible assignments in its input computation, and then ensures that any exit from this block via a continuation passes on the latest values after assignment.

To support this, we add a primitive to our term language:

\KV@do

,commandchars=

{},,

\PY{k+kr}{data} \PY{k+kt}{Exit} \PY{n}{a} \PY{o+ow}{=} \PY{k+kt}{Exit} \PY{k+kt}{Int} \PY{p}{(}\PY{p}{[}\PY{k+kt}{String}\PY{p}{]} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{n}{a}\PY{p}{)}  \PY{k+kr}{type} \PY{k+kt}{CPSTerm} \PY{n}{a} \PY{o+ow}{=} \PY{k+kt}{Term} \PY{k+kt}{Exit} \PY{n}{a}

The Exit primitive is a hole with an index that is matched up to an intermediate continuation variable. The hole is filled based on the assignments to variables given by the [String] argument, which are computed once those assignments are fully known. It is an additional job of the CPS type to record assignments as they occur in computations within a block, so that they can be later applied to the appropriate Exit primitives.

5.1 Call/CC and Loop

The three basic building blocks from which we build all others are two versions of call-with-current-continuation and loop:

\KV@do

,commandchars=

{},,

\PY{n}{callCC\PYZus{}} \PY{o+ow}{::} \PY{p}{(}\PY{k+kt}{CPS} \PY{k+kt}{Void} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Void}\PY{p}{)}             \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{n+nb}{()}  \PY{n}{callCC} \PY{o+ow}{::} \PY{p}{(}\PY{p}{(}\PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Void}\PY{p}{)} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Void}\PY{p}{)}            \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val}  \PY{n}{loop} \PY{o+ow}{::} \PY{p}{(}\PY{k+kt}{CPS} \PY{k+kt}{Void} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Void}\PY{p}{)} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Void}

Each of these functions:

inputs a block; 2. 2.

generates its CPS term; 3. 3.

computes its assignments; 4. 4.

nests the CPS’ed term inside its successor block.

Specifically, callCC_ inputs a block which depends on an exit into the successor block; the function callCC inputs a block which depends on an exit which additionally receives a value to throw to the next block. Finally, loop inputs a block which depends on an exit into itself.

For example, if f takes an exit $k$ and produces a CPS’d term $\phi(k)$ with assignments to variables $x$ and $y$, then callCC_ f will produce a CPS’d term

[TABLE]

while loop f will produce a CPS’d term

[TABLE]

5.2 Binding and assignment

Assignments can only be made if we can statically determine how they should be propagated to successor blocks. In the original concept of ProofScript, this was controlled with the introduction of “linear scopes".

For our CPS type, the constraints are enforced mostly be the use of our basic building blocks defined in the previous section, with one additional constraint: the bodies of abstractions, effectively being dynamic nodes in the control flow, are outright not allowed to assign to variables defined outside their scope. This is enforced by ensuring that every CPS value tracks an environment of assignable variables, which can be cleared whenever we compute the CPS of an abstraction.

\KV@do

,commandchars=

{},,

\PY{n}{val} \PY{o+ow}{::} \PY{k+kt}{String} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val}  \PY{n}{assign} \PY{o+ow}{::} \PY{k+kt}{String} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{n+nb}{()}  \PY{n}{abs} \PY{o+ow}{::} \PY{k+kt}{String} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val}

The expression val x rhs body evaluates rhs and then evaluates body in an environment which contains a new assignable binding of x using the function withLocal. The implementation makes use of a number of functions defined so far:

\KV@do

,commandchars=

{},,

\PY{n}{val} \PY{o+ow}{::} \PY{k+kt}{String} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val}  \PY{n}{val} \PY{n}{x} \PY{n}{rhs} \PY{n}{body} \PY{o+ow}{=} \PY{n}{callCC} \PY{o}{\PYZdl{}} \PY{n+nf}{\PYZbs{}}\PY{n}{k} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kr}{do}    \PY{n}{rhs\PYZsq{}} \PY{o+ow}{\PYZlt{}\PYZhy{}} \PY{n}{rhs}    \PY{n}{nest} \PY{p}{(}\PY{n+nf}{\PYZbs{}}\PY{n}{inner} \PY{o+ow}{\PYZhy{}\PYZgt{}}            \PY{k+kt}{App} \PY{p}{(}\PY{k+kt}{Abs} \PY{p}{(}\PY{k+kt}{Bnd} \PY{n}{x}\PY{p}{)}                 \PY{p}{(}\PY{n}{abstract} \PY{p}{(}\PY{o}{==} \PY{k+kt}{Free} \PY{n}{x}\PY{p}{)} \PY{n}{inner}\PY{p}{)}\PY{p}{)}            \PY{p}{(}\PY{k+kt}{V} \PY{n}{rhs\PYZsq{}}\PY{p}{)}\PY{p}{)}    \PY{n}{withLocal} \PY{n}{x} \PY{n}{body}    \PY{n}{k} \PY{n}{body}

The function assign is the basic primitive statement, as indicated by its result type CPS (). Its definition checks whether the variable is assignable, establishes a new binding for the variable, and registers a new assignment with a function tell:

\KV@do

,commandchars=

{},,

\PY{n}{assign} \PY{o+ow}{::} \PY{k+kt}{String} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{n+nb}{()}  \PY{n}{assign} \PY{n}{x} \PY{n}{rhs} \PY{o+ow}{=} \PY{k+kr}{do}    \PY{n}{inScope} \PY{o+ow}{\PYZlt{}\PYZhy{}} \PY{n}{flip} \PY{n}{elem} \PY{o}{\PYZlt{}\PYZdl{}\PYZgt{}} \PY{n}{ask}    \PY{k+kr}{if} \PY{n}{inScope} \PY{n}{x} \PY{k+kr}{then} \PY{k+kr}{do}      \PY{n}{rhs\PYZsq{}} \PY{o+ow}{\PYZlt{}\PYZhy{}} \PY{n}{rhs}      \PY{n}{nest} \PY{p}{(}\PY{n+nf}{\PYZbs{}}\PY{n}{inner} \PY{o+ow}{\PYZhy{}\PYZgt{}}              \PY{k+kt}{App} \PY{p}{(}\PY{k+kt}{Abs} \PY{p}{(}\PY{k+kt}{Bnd} \PY{n}{x}\PY{p}{)}                   \PY{p}{(}\PY{n}{abstract} \PY{p}{(}\PY{o}{==} \PY{k+kt}{Free} \PY{n}{x}\PY{p}{)} \PY{n}{inner}\PY{p}{)}\PY{p}{)}              \PY{p}{(}\PY{n}{pure} \PY{n}{rhs\PYZsq{}}\PY{p}{)}\PY{p}{)}      \PY{n}{tell} \PY{p}{(}\PY{n}{mempty}\PY{p}{,} \PY{p}{[}\PY{n}{x}\PY{p}{]}\PY{p}{)}      \PY{k+kr}{else} \PY{n+ne}{error} \PY{p}{(}\PY{n}{x} \PY{o}{++} \PY{l+s}{\PYZdq{}}\PY{l+s}{ cannot be assigned here.}\PY{l+s}{\PYZdq{}}\PY{p}{)}

5.3 Example

The following code is taken from the original language specification for "Babel-17", a language developed by Obua Babel17 :

\KV@do

,commandchars=

{},,

a =\PYZgt{} b =\PYZgt{}    if a == 0 then      b    else      val a = a        while b != 0 do          if a \PYZgt{} b then             a = a \PYZhy{} b          else b = b \PYZhy{} a        end      end    a  end

To show how this code can be expressed by a CPS value, we’ll first assume we have the following primitive functions to hand:

\KV@do

,commandchars=

{},,

\PY{n}{eq} \PY{o+ow}{::} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val}  \PY{n}{gq} \PY{o+ow}{::} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val}  \PY{n}{sub} \PY{o+ow}{::} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val}  \PY{n}{not} \PY{o+ow}{::} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} as well as the following control structures

\KV@do

,commandchars=

{},,

\PY{n}{cond} \PY{o+ow}{::} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{k+kt}{Val}  \PY{n}{cond\PYZus{}} \PY{o+ow}{::} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{n+nb}{()} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{n+nb}{()} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{n+nb}{()}

We can then define a while loop in terms of callCC_ and loop:

\KV@do

,commandchars=

{},,

\PY{n}{while} \PY{o+ow}{::} \PY{k+kt}{CPS} \PY{k+kt}{Val} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{n}{a} \PY{o+ow}{\PYZhy{}\PYZgt{}} \PY{k+kt}{CPS} \PY{n+nb}{()}  \PY{n}{while} \PY{n}{b} \PY{n}{body} \PY{o+ow}{=}    \PY{n}{callCC\PYZus{}} \PY{p}{(}\PY{n+nf}{\PYZbs{}}\PY{n}{break} \PY{o+ow}{\PYZhy{}\PYZgt{}}               \PY{n}{loop} \PY{p}{(}\PY{n+nf}{\PYZbs{}}\PY{n}{cont} \PY{o+ow}{\PYZhy{}\PYZgt{}}                       \PY{n}{cond} \PY{n}{b} \PY{p}{(}\PY{n}{body} \PY{o}{\PYZgt{}\PYZgt{}} \PY{n}{cont}\PY{p}{)} \PY{n}{break}\PY{p}{)}\PY{p}{)}

And thus we can write:

\KV@do

,commandchars=

{},,

\PY{n}{abs} \PY{l+s}{\PYZdq{}}\PY{l+s}{a}\PY{l+s}{\PYZdq{}} \PY{o}{\PYZdl{}} \PY{n}{abs} \PY{l+s}{\PYZdq{}}\PY{l+s}{b}\PY{l+s}{\PYZdq{}} \PY{o}{\PYZdl{}}    \PY{n}{cond} \PY{p}{(}\PY{n}{eq} \PY{l+s}{\PYZdq{}}\PY{l+s}{a}\PY{l+s}{\PYZdq{}} \PY{l+s}{\PYZdq{}}\PY{l+s}{0}\PY{l+s}{\PYZdq{}}\PY{p}{)}          \PY{l+s}{\PYZdq{}}\PY{l+s}{b}\PY{l+s}{\PYZdq{}}          \PY{p}{(}\PY{k+kr}{do} \PY{n}{val} \PY{l+s}{\PYZdq{}}\PY{l+s}{a}\PY{l+s}{\PYZdq{}} \PY{l+s}{\PYZdq{}}\PY{l+s}{a}\PY{l+s}{\PYZdq{}} \PY{o}{\PYZdl{}} \PY{k+kr}{do}                \PY{n}{while} \PY{p}{(}\PY{n}{not} \PY{p}{(}\PY{n}{eq} \PY{l+s}{\PYZdq{}}\PY{l+s}{b}\PY{l+s}{\PYZdq{}} \PY{l+s}{\PYZdq{}}\PY{l+s}{0}\PY{l+s}{\PYZdq{}}\PY{p}{)}\PY{p}{)} \PY{o}{\PYZdl{}} \PY{k+kr}{do}                  \PY{n}{cond\PYZus{}} \PY{p}{(}\PY{n}{gq} \PY{l+s}{\PYZdq{}}\PY{l+s}{a}\PY{l+s}{\PYZdq{}} \PY{l+s}{\PYZdq{}}\PY{l+s}{b}\PY{l+s}{\PYZdq{}}\PY{p}{)}                        \PY{p}{(}\PY{n}{assign} \PY{l+s}{\PYZdq{}}\PY{l+s}{a}\PY{l+s}{\PYZdq{}} \PY{p}{(}\PY{n}{sub} \PY{l+s}{\PYZdq{}}\PY{l+s}{a}\PY{l+s}{\PYZdq{}} \PY{l+s}{\PYZdq{}}\PY{l+s}{b}\PY{l+s}{\PYZdq{}}\PY{p}{)}\PY{p}{)}                        \PY{p}{(}\PY{n}{assign} \PY{l+s}{\PYZdq{}}\PY{l+s}{b}\PY{l+s}{\PYZdq{}} \PY{p}{(}\PY{n}{sub} \PY{l+s}{\PYZdq{}}\PY{l+s}{b}\PY{l+s}{\PYZdq{}} \PY{l+s}{\PYZdq{}}\PY{l+s}{a}\PY{l+s}{\PYZdq{}}\PY{p}{)}\PY{p}{)}                \PY{l+s}{\PYZdq{}}\PY{l+s}{a}\PY{l+s}{\PYZdq{}}\PY{p}{)}

Notice how similar this code is to the source language, despite being shallow embedded in another functional language. The combinators generate a single pure lambda term, where assignments are replaced by variable rebinding and their final values propagated through continuations. In fact, after beta-eta reduction, we obtain the concise and pure lambda term:

[TABLE]

6 Conclusion

As we have shown, a pure functional language which supports assignment and structured programming constructs can be embedded as a datatype CPS whose combination closely resembles our source language ProofScript. As such, the datatype CPS can be used to express the semantics of ProofScript, as well as acting as the first compilation phase in our production compiler. The datatype ensures a certain amount of type-safety, distinguishing as it does between expressions of type CPS Val, statements of type CPS () and computations that have exited via a continuation of type CPS Void.

The basic ingredients here are a function to implement two basic control flow mechanisms: looping and call-with-current-continuation. From these, a variety of other control flow constructs can be obtained. The coordination of assignments through these is automatically and safely handled by the basic datatype, leaving us working with what feels like a pure but structured imperative language.

In further work, we would like to formally investigate and explore our intuition that the resulting language and the way it structures control flow closely resembles static-single assignment.