Pure imperative programming

Two intensively studied intermediate representations in compiler theory are Static Single Assignment form (SSA) and CPS translations, and Richard Kelsey's 1995 paper, A Correspondence Between Continuation Passing Style and Static Single Assignment Form (.ps.gz) shows a nearly complete, exact equivalence between the two IRs.

The correspondence shows how the imperatively expressed SSA can be regarded as side-effect free, and Andrew Appel has pushed this idea to claim that SSA is functional programming. This result is of clear relevance to discussions turning on "what is purity?", such as here.

As an aside, the Wikipedia article Static Single Assignment form is rather good.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Admin: which department?

I classified this as "Theory" since compiler theory seemed the most obvious subject area. Might LtU benefit from compiler theory as a department of its own?

Usually I used the

Usually I used the implementation dept. for things related to intermediate languages, VMs etc. But in this case I think it makes sense to put the result in the theory dept. as well. I am not sure if there is a real reason for a separate dept. for compiler theory.

um.. what's the ado about?

Why are these results considered to be surprising?


also, calling SSA "imperative"

Calling SSA imperative is a stretch.


Is it?

Then why was it necessary for Appel to write "SSA is Functional Programming?" I think that calling SSA "imperative" is justified by SSA's popular use as an intermediate representation for imperative languages such as C and C++. But somewhere between monads and linear logic, I think we're coming to a fuller appreciation that "pure," "functional," and "imperative" aren't quite as clear-cut terms as many of us (myself included) tend to treat them as.


Note that these are papers from around 1995-1998, which Charles is posting since they've apparently never had their own story here. At this point they're more "classic" than "surprising".

Classic = surprising + age

Surprisingly classic? Classically surprising?


Errata for A Correspondence Between ....

I tried to implement the conversion to CPS style, and I noticed a bug in the conversion function F. In

F([(E ...), C]) = (let ((v (E ...))) (j v)), if C = j and j is bound by letrec,

notice that (E ...) is not valid grammar in the CPS language. Any thoughts, or any errata for this paper?