Communications - February 2012

Doi: 10.1145/2076450.2076471

Technical Perspective
compiling What to How
By Rastislav Bodik

iF a PrOgraMMer is lucky, her program requires no coding: She specifies the desired property and an existing algorithm computes a result that meets her property. Examples include finding a string with regular expressions, solving systems of linear equations, and determining whether a Boolean formula is satisfiable. Such declarative programming reuses algorithms that we might call solvers. Whenever our problem is expressible as a property understood by a solver, we are free to say what should be computed without saying how to compute it.

Not all problems lend themselves to declarative programming, of course. For some problems it may be faster and more natural to write the program rather than its specification. Large programs, like document editors, will never be fully specified. Then there are undecidable properties for which it is impossible to build a solver.

Given these limitations, should we even contemplate declarative programming? The following paper by Viktor Kuncak et al. integrates declarative programming into a general-purpose language, allowing one to escape the host language when a subproblem can be solved declaratively.

Their first contribution is language constructs that make the Scala host language more powerful without making declarative properties obtrusive. For example, their case statement almost hides the fact that a constraint is being solved at runtime: this code decides whether i is even or odd by determining whether there exists a solution to the equations 2*j=i and 2*j+ 1=i, yet the code closely resembles the standard pattern matching:

match i { case 2*j => print(“even”) case 2*j+ 1 => print(“odd”)

}

In declarative programming, it is
easy to write buggy properties—those
that permit either too many or no sat-
isfying results. As the second contri-
bution, the paper develops debugging
support for both kinds of errors. When
a specification is under-constrained,
there exists an input that permits
multiple legal results. To help deter-
mine whether this freedom consti-
tutes undesirable non-determinism,
the compiler looks for such an input.
If it exists, the compiler computes two
distinct results, which might hint at
what constraint is missing in the prop-
erty. When a specification is over-con-
strained, there is an input that permits
no legal result. The compiler computes
the set of such inputs, and describes
the set symbolically with a predicate.
Both warnings are delivered to the pro-
grammer before the program is execut-
ed, reducing the need for testing.