Thoughts on
Declarativeness
What it means, when to use it, and how to shape it
DSLs are supposed to be
“declarative”. People say this, but it is not clear what they mean with it. So
let us unpack this a little bit. What does it mean for a language to be
declarative? Here is the definition from
Wikipedia:
In computer
science, declarative programming is a programming
paradigm— a style of building the structure and elements of computer
programs — that expresses the logic of a computation without
describing its control flow.
Ok, this is useful. But then,
is a pure functional language declarative? After all, it has trivial control
flow (the call graph is the control flow graph) and no side-effects. If so,
what is the difference between functional and declarative? Wikipedia continues
to say
[describe] what the program must accomplish in
terms of the problem domain, rather than describe how to
accomplish it as a sequence of the programming language primitives.
This is essentially the
definition of a (good) DSL. So are all DSLs declarative?
Another definition I have
seen points out that a declarative program is one that does not even have a
predefined execution order (a functional program has this). In other words,
there is some kind of “engine” that processes the program by finding out an
efficient way of “working with the program” to find a solution.
Solvers & Constraint-based
Programming
Solvers are examples of such
engines. They take as input a couple of equations with free variables, and try
to find value assignments to these variables that satisfy all the equations.
For mathematical equations, we know the problem from school:
Eq1: 2 * x == 3 * y
Eq2: x + 2 == 5
Eq3: 3 == y + 1
A solution for this set of
equations is x := 3, y := 2. Solvers that solve this
kind of equations, are called SMT solvers. SMT stands for “Satisfiability
Modulo Theories”; the “Theories” part relates to the set of abstractions it can
work with. For example, in addition to to arithmetics, they can also work with
other “theories”, such as logic or collections. Modern SMT solvers, such
as Z3, can
work with huge sets of equations and large numbers of free variables, while
still solving them in very short time (sub-second). For more details on the use
of solvers in DSLs, and lots of related work, see Section 5 in the Formal Methods booklet.
Note that these equations do
not imply a direction — they can be solved left to right and right to left,
because they only specify constraints on the variables. This is why this
approach to programming is also called constraint-based programming.
It is possible to encode
structure/graphs as equations (also called relations). Once we have done this,
we can “solve for structure”, i.e., we can find structures that satisfy the
other constraints expressed in the equations. For example, one can express the
data flow graph as a set of relations over the program nodes and then perform
dataflow analyses, ideally incrementally. The INCA paper by
Tamas Szabo, Sebastian Erdweg and yours truly explains how to do this.
Such constraints can also
represent some notion of cost, for example, the needed bandwidth for a network
connection. In this case, a solver is used iteratively. Czarnecki et al. perform
multi-objective optimisations for structural and variable models. A
hello-world example is also in the Formal Methods booklet.
The constraints can also be
used to express structural limitations (such as visibility rules in program
trees). We will return to this later.
This is all very nice. But
solvers have three problems. First, encoding non-trivial problems as equations
can be tough. This is especially true for structures. Second, depending on the
number, size and other particular properties of the equations, the required
memory and/or performance can be a problem — it does get big and slow quickly,
again, especially for structures And finally, because the engine uses all kinds
of heuristics and advanced algorithms to find solutions efficiently, debugging
can be a real nightmare.
State Machines and Model
Checking
Are state machines
declarative? Well, I don’t know. They do encode control flow (in particular, as
reactions to outside events). They also change global state (which is where
their name comes from). And that state potentially evolves differently,
depending on the order (and timing, in timed state-machines) of incoming events.
So this pretty much makes state machines as non-declarative as you can get.
But is this really a useful
definition? One reason why people use state machines is that they can be
analyzed really well. The whole field of temporal logic and model checking (see
Section 6 in the Formal Methods booklet) is about verifying properties on
state machines. The reason why this works is that they make state and the way
it evolves explicit using first-class language constructs. I will discuss model
checking in a future post.
Alternative Definition of
Declarativeness
Let me propose another
definition of declarativeness. It might sound overly pragmatic, but it is
nonetheless useful:
Declarativeness: A declarative language is one that makes
those analyses simple/feasible that are required for the use cases of the
language.
This reemphasises a core idea
underlying the Formal Methods booklet: you should consciously design a
language in a way that makes analyses simpler; usually by making the right
things first class. In the rest of the post I show two examples of meta
languages (i.e., languages used in language definition) that illustrate the
point.
Scopes
In a
language workbench like MPS, programs are represented as graphs. The
containment structure is a tree, but there are cross-references as well. For
example, a Method contains
a Statement, a Statement might
contain a VariableRef (a particular kind of Expression), which in turn references a Variable defined
further up in the method. The language structure only talks about concepts: a VariableRef has a
reference var that points to a Variable. But it
does not specify which variables. Scopes are used to define the set of valid
reference targets (Variables in this example). They are a way of implementing visibility rules
in a language.
Scopes as Functions
A scope can be seen as a
function with the following signature:
fun scope(node<T> n, Reference r): set<U>
In our example, T would be VariableRef, r would
represent the varreference, and U would be Variable. A naive
implementation of a scope can be procedural or functional code that returns,
for example, the set of all Variables in the current method
(let’s ignore order and nested blocks for now) as well as the GlobalVariables in the
current program. The example below encodes the particular reference for which
we define the scope in the name of the function:
fun scope_VariableRef_var(node<VariableRef> n): set<Variable>
= {
n.ancestor<Method>.descendants<Variable> union
n.ancestor<Program>.descendants<GlobalVariable>
}
So far so good. Whenever the
user presses Ctrl-Space to see the set of valid reference targets (or when an
existing reference is validated by the type checker), the system can simply
call this function and use the returned set for display in the menu (or for
testing if the current target is in the set).
Creating Targets
Let us now introduce an
additional requirement. Let’s say, the user wants to reference something that
does not yet exist. Since a projectional editor like MPS establishes references
eagerly (as opposed through lazily resolved names), the target element must
actually exist for us to be able to establish the reference. We can’t
write down a method name (with the intention to call it), and then later fill
in the method; the reference cannot be entered! To still support top down
programming, we have to be able to implicitly create missing targets. So if a
user presses Ctrl-Space in the context of a VariableRef, in addition to
choosing from existing targets (computed by the scope), the tool should provide
one-click actions for creating new targets (through a quick fix or a special
part in the code completion menu).
Here is the catch: the
one-click target creators should create valid targets. So they
have to somehow find out, where in the program which kinds of targets would be
valid and only propose those. Extracting this information from the scope
definition above (or even worse, one written in a procedural language) is
really quite hard.
Solver-based Solution
In some sense, we have to
“forward-evaluate” the scope to find the places where, if a node existed there,
it would be a valid target for the reference. Solvers can do just this. If we
formulate the program structure and the scopes as constraints, transform the
current program to a set of equations and then ask the solver to solve them (in
the right way), this would solve the problem quite elegantly. People have
worked on this, see for example Friedrich Steimann’s work (here, here and in particular, here).
However, the performance and memory requirements, as well as the (from most
developers’ perspectives) non-intuitive way of specifying the constraints makes
this approach challenging in practice. Hundreds of MB or even GBs of memory for
relatively small programs is common. Currently, I cannot see how to use this in
practice.
Structure-based Declarativeness
Consider the following scope
definitions:
scope for VariableRef::var {
navigate
container Method::statements
path
node.ancestor<Method>
navigate
container Program::contents
path
node.ancestor<Program>
of GlobalVariable
}
This has the following
structure and semantics. A scope defines which concept and which reference it
is for (here: var in VariableRef). It then
contains multiple separate definitions of where targets can be found. Each one
specifies a container location (the statements collection
in a Method or the contents of a Program) as well as a path expression
of how to get there from the perspective of the current node. The execution
algorithm is as follows: for each navigate block, execute the path expression
from the current node to get to the container nodes. Then grab all the nodes in
the specified container slot (statements or contents), but only
select those that are of the compatible concept, or those explicitly specified
by the of clause.
For our second use case, the
creation of missing targets, we don’t have to perform any magic: we create an
action for each of the navigate blocks (so in the
example, we’d get two, as expected). To execute the action, we execute exactly
the same path expression to lead us to the container nodes, just as
when we evaluate the scopes. We then create the new nodes in the slot defined
by the container.
For this to work we don’t
need a solver, we do not have to “forward-evaluate” (or solve) anything. The
path expressions can be as complicated as they want to be, we can filter, or
compute anything we want …
path node.ancestor<Method>.where(
it.statements.size < 10
&& !it.name.endsWith(“X”))
… because we always only
evaluate it as a functional program. And there is no performance problem, we
just “execute” code. There are, of course, limitations. We cannot express more
complex structural constraints. But this was not the goal. Below is a screenshot
of a working example of a somewhat more complex set of scoping rules:
Even debugging such scope
definitions is not a real problem, because, again, there is no real advanced
magic going on: it is a mix of function evaluation and some specific (but
straight-forward) debug support for the declarative parts. I will revisit
debugging of these and other DSLs in a future post.
Type Systems
Type systems are primary
candidates for declarativeness. In fact, MPS itself uses a type equations and a
solver to compute types. Let me give an example.
MPS Type System DSL
Imagine you want to compute
the type of the following list:
val l = list(1, 2, 23.3)
The list contains ints and floats, and in most
languages, the resulting type would be list<float> because float is a
supertype of int. In other words, the
resulting type is a list type of least common supertype of the elements of the
list. Here is how MPS expresses this rule:
typing rule for ListLiteral as l {
var T;
foreach e in l.elements {
T :>=: typeof(e)
}
typeof(l) :==:
<ListType(baseType: T)>
}
This code first declares a
type variable T. It then iterates over all elements in the list
literal and adds an equation to the set of equations that
expresses that T must be the same type or a supertype (:>=:) of the type
of the element ewe are currently iterating over. At the end of the foreach we have
created as many equations as there are elements in the list literal, all of
them expressing a constraint on the variable T. Next we
create another equation that expresses that the type of the list literal l (the
thing we are trying to find a type for) must be the same types as (:==:) a ListType whose
base type is T. All of these equations are then fed to a solver
who tries to find a solution for the value of T.
Another example. Consider a
language with type inference. When you declare a variable, it can be
· Only a name and a type; the type of the
variable is then the explicitly given type (var x: int).
· Only a name and an init value; in this case
the type of the variable is inferred from the init expression (var x = 10).
· A name, type and an init expression; the
type is the explicitly given one, but the init expression’s type must be the
same or a subtype of the explicitly given one (var x: int = 10).
The typing rule that
expresses this is given here:
typing rule for Variable as v {
if v.type != null then
typeof(v) :==: typeof(v.type)
else typeof(v)
:==: typeof(v.init)
if v.init != null then
typeof(v.init) :<=: typeof(v)
}
The MPS type system language
is quite powerful. For meaningfully-sized programs it performs well, mostly
because it is updated incrementally. MPS tracks changes to the program and then
selectively adds and removes equations from the set of equations considered by
the solver. The solving itself is also incremental.
The nice thing about the MPS
type system DSL is — surprise! — its declarativeness. MPS supports language
extension and composition, and the type system fits in neatly: and extension
language just adds additional equations (constraints) to the set of type
equations considered by the solver. There’s no fuzz with execution order or
extension points or anything.
However, it has one major
weak spot: debugging. If your type system does not work, there is a debugger.
All it does, essentially, is to visualise the solver state. If you don’t
understand in detail what the solver does, this is rather useless. I have heard
rumours that there is somebody in Jetbrains’ MPS team who understands the
debugger, but I haven’t met the guy yet :-)
Type Systems expressed through Functions
A much simpler way for
expressing type systems is functions: you can imagine every language concept to
essentially have a function typeof that returns its type. In that function you
explicitly call the typeof functions of other nodes. You define the order
explicitly, usually bottom-up! It runs as a simple functional program, with
good performance, and debugging is easy. There’s no constraints, no
execution-order independence, and it is a bit harder to extend (because of the
execution order).Many language workbenches, including Xtext, use this approach.
Structure-based Declarativeness
Let us now look at the
following typing rule for the variable declaration:
typing rule for Variable as v =
primary v.type :>=: secondary
v.init
Here is its semantics: if a v.type is given,
then it becomes the result type; the v.type wins, it is the primary. If no v.type is given,
then the secondarywins, the v.init in this
case. If both are given, the primary still wins, but the secondary must be
the same or a subtype of the primary.
For the list literal example,
the typing rule is:
typing rule for ListLiteral as l =
create ListType[baseType: commonsuper(l.elements)]
}
It is so obvious, I don’t
even have to explain what it does.
Both of these are much
shorter, more expressive, and can be evaluated without a solver. The reason for
this is that we have created direct, first-class abstractions for the relevant
semantics — the language is declarative!
Debugging is straightforward
by the way, the debugger can simply “explain” what is going on: v.type is null, so taking v.init: float.
There is of course an obvious
drawback as well: you have to implement more, and more specific language
abstractions, essentially one for every typing idiom you want to support (or
you provide a fallback onto regular functional programming). However, we expect
there to be fewer than 20 of such idioms to express the vast majority of
relevant type systems. Implementing those with a tool like MPS is not a big
deal — certainly more feasible than implementing a fast solver!
Wrap up
In this post I have
illustrated what I mean by declarative: a language where the analyses I am
interested in are expressed first-class. I have explained the idea based on two
meta languages (for scopes and type systems). Those, by the way, have been
taken from a new set of language definition DSLs we are working on. Stay tuned,
you will read much more of those in the future :-)