Annotations

A definition can be preceded by a number of optional annotations. An annotation consists of the character @, immediately followed by an identifier: for example, @inline.

By convention, the annotations of a definition are written on a separate line.

This section briefly describes the most commonly used annotations, which are listed in lexicographic order below. The list is not complete and is likely to change over time. You may want to bookmark this page for future reference. Most of the omitted annotations have very specialized purposes, such as displaying the intermediate results of compilation or suppressing a particular optimization.

Here is a quick overview of three annotations that are related closely enough to sometimes cause confusion:

• @ondemand does not, by itself, allow you to use higher-order variables but is used to annotate infinite relations that are used “by need.” You may have to combine it with @outline if the infinite relation uses higher-order variables.
• @inline and @outline do allow higher-order variables.
• @inline does not allow recursive definitions, whereas @outline does.
• @outline is generally preferable to @inline. You may have to combine them with @ondemand if the relation is infinite.

See also Combining Annotations.

@function

The main purpose of annotating some relation R with @function is to indicate that R is a function. In some situations this allows the system to perform optimizations that may drastically decrease the computational cost of your application. It’s your responsibility to ensure that R really is a function: the annotation will not always do that for you. If R turns out not to be a function, then the optimized logic may yield incorrect results.

A relation is a function if there is only one value for a given tuple of keys. By default, the value is the last element of a tuple and the keys are all the other elements.

In the example below, F is a function, but G is not:

def F { 1, 10, 101; 2, 10, 200 }
def F { 1, 20, 100 }
 
def G { 1, 10, 101; 2, 10, 200 }
def G { 1, 10, 100 }

In many cases Rel does attempt to automatically make the annotated relation a function. For instance, if you annotate the definition of G in the example above, only one tuple with the keys 1 and 10 will be retained:

// read query
 
@function
def G { 1, 10, 101; 2, 10, 200 }
def G { 1, 10, 100 }
 
def output = G

You may use @function to annotate the first insertion into a base relation. When you later add a new tuple to the base relation, the addition is often preceded by the automatic deletion of an existing tuple that has the same keys and a different value. This is illustrated in the following example:

// write query
 
@function
def insert[:BaseF] = 1, 1 ; 2, 2 ; 1, 0 ; 3, 3

// read query
 
def output = BaseF

// write query
 
def insert[:BaseF] = 1, 2; 2, 1

// read query
 
def output = BaseF

For derived relations, there is no sequence of insertions and/or deletions. A derived relation is always considered a whole, even if it is defined piecemeal in different transactions. For instance:

// model
 
@function
def DerF = 1, 1 ; 2, 2 ; 3, 3

// read query
 
def output = DerF

// model
 
def DerF = 1, 2; 2, 1

// read query
 
def output = DerF

If there is more than one tuple with the same key, the lexicographically smaller one is kept in the relation.

@inline

When a definition of relation R is annotated with @inline, the annotation makes Rel treat the definition differently. The relation R is not materialized; instead, its definition is inlined, or expanded at every place where it is used. More precisely, a copy of the body of the definition of R replaces every relational application of R, after replacing the parameters with the appropriate arguments.

Consider the following example:

@inline
def P[x, y] = x * x + y
def Q[x] = P[x, x] + P[2.0, 3.0]

The annotation makes the definition of Q equivalent to:

def Q[x] = x * x + x + 2.0 * 2.0 + 3.0

An inlined definition — or a series of such definitions — cannot be recursive. Such direct or indirect recursion would lead to infinite expansion, so it is treated as an error.

The following example features indirect recursion: P uses Q, and Q uses P.

// read query
 
@ondemand
def P[x in Int] = Q[x] * 2
@ondemand
def Q[x in Int] = if x > 1 then P[x - 1] else 1 end
def output = P[4]

If you change the annotations on either P or Q to @inline, the result will be the same. But if you add @inline to both the definitions, the compiler will raise an error.

An inlined definition can have occurrences of variables that are not grounded, as long as they are grounded in the definitions in which it is expanded. One consequence of this is that an inlined definition that appeared to be correct may suddenly cause an error when used in a new way.

For instance, in the example above, you can replace either one of the occurrences of @ondemand with @inline. If the definition of P and/or Q is deprived of annotations, x will be ungrounded and Rel will raise an error.

You can use the annotation @inline to annotate nonrecursive higher-order definitions, that is, definitions of relations whose parameters are other relations. In general, however, it is preferable to use @outline for this purpose. See Higher-Order Definitions for more details.

You can also use the annotation @inline in the definitions of parameterized modules. It is best to use @outline there, as well.

The annotation @inline causes the definition of a relation R to be treated, roughly speaking, as a C macro. That is, the definition of R is expanded wherever R is used. This is why it cannot be used for recursive definitions. Consider the following example, which is yet another version of transitive closure:

@inline def tc[E] = E; E . (tc[E])
def edges = (1, 2); (2, 3); (3, 4)
def output = tc[edges]

The compiler rewrites this as:

def output = edges; edges . (tc[edges])

This, in turn, is rewritten as:

def output = edges; edges . (edges; edges . (tc[edges])))

There is no end to such rewriting, so the compiler reports an error.

Compare this to the same example described in section @outline.

Automatic Inlining

Some definitions are inlined by the compiler even if they are not annotated with @inline. This happens, in particular, when:

• The compiler can determine that the arguments of a relation are ungrounded.
• The definition of that relation is not recursive.
• The types of variables are given or can be inferred.

For instance, consider the following definition of an infinite relation f:

def f[x in Int] = x * x + x

The partial relational application f[10] will be replaced with the expression 10 * 10 + 10, whose value is 110.

See also the example at the end of Grounded Variables.

When in doubt about whether a definition will be automatically inlined, you can always annotate it with @inline.

@ondemand

This annotation prevents Rel from materializing the defined relation. Rel computes only those parts of the relation that are actually used. This is particularly useful if the relation is infinite.

The compiler achieves this by performing a demand transformation, which will be explained in this section.

In simple cases there is no need to add the annotation, as the compiler can infer that certain infinite relations must be subjected to a demand transformation. Using @ondemand in those cases does no harm.

The example below implements the Library relation range in Rel. The relation my_range is infinite, so, if the annotation is missing, Rel produces an error message informing you that low, high, and stride are ungrounded. The annotation allows my_range to be materialized to just the subset that is relevant for the given arguments:

// read query
 
@ondemand
def my_range[low in Int, high in Int, stride in Int] = low, low <= high
def my_range[low in Int, high in Int, stride in Int] =
    my_range[low + stride, high, stride], low < high
 
def output = my_range[1, 6, 2]

Notice that in this case you cannot replace @ondemand with @inline, because the definition is recursive.

By annotating the definition of some relation R with @ondemand you inform the compiler that it should perform a demand transformation, that is, that it should rewrite the definition in such a way that R becomes finite. The rewriting takes into account the ways in which R is used.

Consider the following example, in which the @ondemand annotation is omitted because the compiler infers it for sufficiently simple relations:

def f[x in Int] = 2*x     // Infinite relation
def output = f[3] + f[4]

The compiler rewrites it to something similar to the following:

def f[x in Int] = 2 * x, demand_of_f(x)
def demand_of_f(x) { x = 3 or x = 4 }
def output = f[3] + f[4]

The relation demand_of_f is finite, so the addition of the conjunct demand_of_f to the body of the definition of f causes f to become finite.

If the infinite relation is recursive, the rewriting must be a little more involved. The following is a definition of the factorial function:

@ondemand
def f[0] = 1
def f[n] = n * f[n - 1], n > 0
 
def output = f[5]

The compiler rewrites this more or less as follows:

// read query
 
def f[0] = 1,  demand_of_f_1(0)
def f[n] = n * f[n - 1], n > 0,  demand_of_f_1(n)
 
def demand_of_f_1(m) { m = n - 1, n > 0,  demand_of_f_1(n) from n }
def demand_of_f_1 = 5
 
def output:aux = demand_of_f_1
def output:all = f

The relation demand_of_f_1 is recursively defined, but it is finite. It serves to make the rewritten f finite, as well.

@outline

The annotation @outline supports higher-order definitions. A higher-order definition is a definition of a relation, some of whose parameters represent non-singleton relations. See Higher-Order Definitions for more details.

Specifically, @outline directs the compiler to use the annotated definition as a template from which to generate a first-order definition that is specialized on the higher-order parameters. For example, R is the higher-order parameter in the following definitions of a transitive closure relation:

// read query
 
// Compute the transitive closure of a binary relation.
@outline
def transitive_closure[R] = R
@outline
def transitive_closure[R] = R . (transitive_closure[R])
 
def edges = (1, 2); (2, 3); (3, 4)
 
def output = transitive_closure[edges]

The compiler rewrites this to a first-order form similar to the following:

// read query
 
def transitive_closure_edges = edges
def transitive_closure_edges = edges . (transitive_closure_edges)
 
def edges = (1, 2); (2, 3); (3, 4)
 
def output = transitive_closure_edges

This example features the composition operator. Notice the parentheses in the second higher-order definition above. If you omit them, the definition will be syntactically incorrect. A different version of transitive_closure is shown in Higher-Order Definitions.

The annotation @outline is necessary in the second definition above, because the definition is recursive. If a higher-order definition is not directly or indirectly recursive, you can replace the annotation @outline with @inline. One of the two annotations must be used for any higher-order definition.

If a higher-order definition is not recursive, then @inline is sometimes preferable to @outline, because the former can help avoid materialization of a large relation. An example of this phenomenon is discussed in Combining Annotations.

All else being equal, it is best to use @outline rather than @inline for higher-order definitions.

This also applies to annotations of parameterized modules.

@static

You can use this annotation for integrity constraints that can be evaluated statically, that is, on the basis of the schema, without looking at the data. If the compiler cannot evaluate an integrity constraint statically, it will ignore the annotation. See the @static annotation in the Integrity Constraints concept guide.

Combining Annotations

The compiler allows the three annotations, @inline, @ondemand, and @outline to be combined. However, it makes sense to combine only two of these: @outline and @ondemand. The order in which you write them does not matter. The annotation @outline always takes effect before @ondemand.

Combining @outline with @ondemand, even when not necessary, can affect execution time. Here is a simple example:

@outline
def my_add(R, x, y, z) {
  R(x) and R(y)
  and z = x + y
}
def output = my_add[range[1, 10000, 1], 3, 4]

This can take a noticeable time to compute, because the relation that is the first argument of my_add has ten thousand elements and is materialized. After adding @ondemand, the relation my_add will be rewritten in a way that will prevent this materialization from occurring, so the computation will become noticeably faster:

@outline @ondemand
def my_add(R, x, y, z) {
  R(x) and R(y)
  and z = x + y
}
def output = my_add[range[1, 10000, 1], 3, 4]

In this case you can achieve a very similar speedup by replacing @outline with @inline.

In general, it is difficult to formulate hard-and-fast rules for such tweaks, and you will not always need them. Nonetheless, a little experimentation can help improve your model in the shorter term.

Next: Specialization