Imperative Functional Programs that Explain their Work

Imperative Functional Programs that Explain their Work
Wilmer Ricciotti, Jan Stolarek, Roly Perera, James Cheney
submitted on arXiv on 22 May 2017

Program slicing provides explanations that illustrate how program outputs were produced from inputs. We build on an approach introduced in prior work by Perera et al., where dynamic slicing was defined for pure higher-order functional programs as a Galois connection between lattices of partial inputs and partial outputs. We extend this approach to imperative functional programs that combine higher-order programming with references and exceptions. We present proofs of correctness and optimality of our approach and a proof-of-concept implementation and experimental evaluation.

Dynamic slicing answers the following question: if I only care about these specific part of the trace of my program execution, what are the only parts of the source program that I need to look at? For example, if the output of the program is a pair, can you show me that parts of the source that impacted the computation of the first component? If a part of the code is not involved in the trace, or not in the part of the trace that you care about, it is removed from the partial code returned by slicing.

What I like about this work is that there is a very nice algebraic characterization of what slicing is (the Galois connection), that guides you in how you implement your slicing algorithm, and also serves as a specification to convince yourself that it is correct -- and "optimal", it actually removes all the program parts that are irrelevant. This characterization already existed in previous work (Functional Programs that Explain Their Work, Roly Perera, Umut Acar, James cheney, Paul Blain Levy, 2012), but it was done in a purely functional setting. It wasn't clear (to me) whether the nice formulation was restricted to this nice language, or whether the technique itself would scale to a less structured language. This paper extends it to effectful ML (mutable references and exceptions), and there it is much easier to see that it remains elegant and yet can scale to typical effectful programming languages.

The key to the algebraic characterization is to recognize two order structures, one on source program fragment, and the other on traces. Program fragments are programs with hole, and a fragment is smaller than another if it has more holes. You can think of the hole as "I don't know -- or I don't care -- what the program does in this part", so the order is "being more or less defined". Traces are also partial traces with holes, where the holes means "I don't know -- or I don't care -- what happens in this part of the trace". The double "don't know" and "don't care" nature of the ordering is essential: the Galois connection specifies a slicer (that goes from the part of a trace you care about to the parts of a program you should care about) by relating it to an evaluator (that goes from the part of the program you know about to the parts of the trace you can know about). This specification is simple because we are all familiar with what evaluators are.

Comment viewing options

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

Galois connections

This is a cool paper, but it always makes me sad that such an important concept (which generalizes to adjunctions in category theory) is hidden behind the terrible jargon "Galois connection". Ultimately it states something obvious enough that it almost sounds redundant in everyday language (e.g in this case):

F = the least input program that produced _
G = the greatest output trace of _

 o <= the greatest output trace of the least input program that produced o // o <= G(F(o))

the least input program that produced the greatest output trace of i <= i // F(G(i) <= i

But the "everyday language"

But the "everyday language" is a bit tortured: is the second statement correct? It is quite difficult to parse which program and which trace on the left-hand-side of the condition. I wonder if translating it into "natural" language has obscured which ordering relations apply to particular clauses in that sentence. I can only interpret it by trying to project it back on to the definition of a Galois Connection. I do not think it makes sense independently.

I am curious about the general understandability of the terminology. The term "Galois Connection" is definitely opaque to most programmers - but how many of them would be familiar with adjunctions in category theory? The idea of preserving ordering relations through a pair of maps is simple enough for most programmers to understand, but the formal definition of it would look overly scary until it is explained in a more familiar setting.

Yes I agree

I agree it sounds stilted in everyday language - just like inverses do:

The opposite of the opposite of down = down

My point was that that's what you should expect out of a Galois connection (which is the fundamental idea: it's the best approximation of an inverse).

Try this one:

F = the _ of cars
G = the _ of watches

the Rolex of cars of watches <= Rolex
Cadillac <= the Cadillac of watches of cars 
but how many of them would be familiar with adjunctions in category theory?

Oh man, category theory jargon is probably even worse tbh.

I guess my point is that these concepts are so fundamental they demand to be translated into more accessible language.

I can't read your example

I can't read your example without parenthesis - limits in the clarity of natural language rather than your expression :).

The definition in abstract interpretation is expressed a little differently : \(x \leq f(g(x))\) and \(y \leq g(f(y))\) allows a description of what the combined effect of pairs of mappings creates. This was how it was taught to us in the specific case of abstracting/concretising value/abstract-values. Explained that way (using set-inclusions as a specific ordering) rather than more general orderings seemed quite straight-forward. It also permits intuitive diagrams to illustrate the concept easily.

The expression in the paper: \(f(x)\leq y \iff x \leq g(y)\) is certainly more compact as a definition, but I prefer the partly unrolled version for conveying the understanding of what it means. As you stated above, the fundamental idea is that it is an approximation of an inverse, although I would think of it as a sound approximation of an inverse rather than a "best" approximation. Probably just my understanding of "best" as I would think of that as minimizing the information loss - i.e. the approximation closest to an exact inverse.

Oystein Ore the culprit

Galois Connexions by Oystein Ore, 1942. Obviously, for the type of people who choose mathematics as a profession such jargon is not much of an obstruction, but it severely limits accessibility for the broader audience - which in today's world includes millions of programmers who could benefit.