Home

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.

By Charles Stewart at 2008-06-20 09:56 | Implementation | Theory | other blogs | 17279 reads

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?

By Charles Stewart at Fri, 2008-06-20 09:58 | login or register to post comments

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.

By Ehud Lamm at Fri, 2008-06-20 15:16 | login or register to post comments

um.. what's the ado about?

Why are these results considered to be surprising?

-t

By Thomas Lord at Fri, 2008-06-20 23:46 | login or register to post comments

also, calling SSA "imperative"

Calling SSA imperative is a stretch.

-t

By Thomas Lord at Fri, 2008-06-20 23:49 | login or register to post comments

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.

By Paul Snively at Sat, 2008-06-21 15:19 | login or register to post comments

Classic

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".

By Anton van Straaten at Sat, 2008-06-21 08:25 | login or register to post comments

Classic = surprising + age

Surprisingly classic? Classically surprising?

By Daniel Yokomizo at Sat, 2008-06-21 12:08 | login or register to post comments

Also

A Functional Perspective on SSA Optimisation Algorithms

and if you are into this kind of thing,
Static Single Information from a Functional Perspective

By Derek Elkins at Sat, 2008-06-21 00:14 | login or register to post comments

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?

PKE.

By Pal-Kristian Engstad at Sun, 2008-06-22 19:29 | login or register to post comments