We present a partial evaluator for functional logic programs written in Curry. In contrast to previous approaches to the partial evaluation of functional logic programs, we take into account the features used in contemporary Curry programs, in particular, non-deterministic operations and recursive let expressions. For this purpose, we base our partial evaluator on FlatCurry, an intermediate language for the representation of Curry programs. We sketch our approach and present initial benchmarks of our implementation.
Partial evaluation of programs is a technique to anticipate the evaluation of computations once at compile time instead of performing them (possibly several times) at run time. This is possible if some part of the input data, also called static data, is known at compile time. In this case, some parts of the program are evaluated so that a residual program, i.e., a specialized version of the original one, is returned. Since some computations have been performed at compile time, the run time of the specialized program could be considerably decreased. The static data does not need to be some user input, but can also be subexpressions in the original program. Offline partial evaluators obtain information about static data from a separate static analysis phase (binding-time analysis), whereas online partial evaluators obtain this information on the fly and propagate it during the partial evaluation process. In this work we follow the online partial evaluation approach.
Partial evaluation has already been studied for different kinds of programming
languages, like functional languages, logic languages, as well as for combined functional
logic languages. An interesting aspect of the partial evaluation of functional logic
programs is the fact that the effects of supercompilation [
Thanks to this insight, partial evaluators for functional logic languages can be
constructed with techniques similarly to the implementation of these languages. For
instance, Albert et al. [
In order to deal with realistic Curry programs, it is crucial for a partial evaluator to
cover the full source language, including both logic features such as non-determinism
and functional features such as recursive let expressions. Therefore, we extend in this
work the partial evaluator of Albert et al. [
We start with an introduction to the functional logic language Curry in Sect. 2 before we sketch the structure of the partial evaluator in Sect. 3. The partial evaluation scheme is presented in Sect. 4, whereas control issues are discussed in Sect. 5. We evaluate our implementation with some benchmarks in Sect. 6 before we conclude in Sect. 7. 2
We briefly review the basic concepts of the functional logic language Curry. More
details can be found in recent surveys on functional logic programming [
The syntax of Curry [
If non-deterministic operations are used as arguments in other operations, a semantical ambiguity might occur. Consider the operation
double x = x + x and the expression “double coin”. If we evaluated this expression by term rewriting, we could have the reduction double coin
coin + coin
→ → → →
leading to the unintended result 1. Note that this result cannot be obtained with a strict
reduction strategy where arguments are evaluated prior to the function calls. In order
to avoid dependencies on the evaluation strategies and exclude such unintended results,
Curry is based on the rewriting logic CRWL, proposed by González-Moreno et al. [
Before describing the details of the partial evaluation process, we provide an overview
of the partial evaluator and its usage. Since our partial evaluator is an extension of the
first partial evaluator for Curry described in [
Our partial evaluator is intended to specialize some parts of a given input program in order to create an optimized, residual program. In order to support the specification of expressions to be optimized, we assume that these expressions are annotated with PEVAL. For example, we assume a program which contains the function definition main xs = map (twice square) xs We can then annotate the main expression (or parts of it) as follows:
main xs = PEVAL (map (twice square) xs) Actually, PEVAL is the identity function, i.e., it has the type a → a. As a consequence, annotations with PEVAL do not change the semantics of the original program. After annotating the program, the process of partial evaluation is fully automatic. The process itself consists of the following phases (depicted in Fig. 1): 1. The partial evaluator is called for a given program, containing annotated expressions as described above. This source program is converted into the standard intermediate representation for Curry programs, called FlatCurry (see Sect. 4.1). 2. The process continues by extracting the set of annotated expressions and creating a copy of the original program without annotations. 3. Both form the input for the partial evaluation phase, which is later described. 4. The output of the partial evaluation is a set of semantically equivalent, potentially more efficient expressions. These expressions are converted to new function definitions to allow reuse, a process called renaming. 5. The evaluation process tends to produce some “intermediate” functions which only pass their parameters to another function. Therefore, the process is finished by a compression phase which removes such intermediate functions by inlining and simplifies expressions to produce a more efficient and legible result. 6. Finally, the annotated expressions of the form (PEVAL e) are replaced with their (hopefully more efficient) equivalents e′, where e′ is the renaming of e. This optimized program is then stored as a FlatCurry program.
Annotated Curry program
Final FlatCurry program (1) (6)
Annotated FlatCurry program
(2) Compressed definitions
Annotated expressions Program without annotations (5) (3) Residual expressions
(4) New function definitions For instance, with the usual definitions of map, twice, and square, the example above is transformed into main xs = map0 xs map0 xs = case xs of [] y:ys → [] → let z = (y*y) in (z*z) : map0 ys so that the overhead of the higher-order operations map and twice is eliminated.
The fact that the partial evaluator internally operates on the FlatCurry format is no
restriction, since this format is used by current Curry compilers anyway, e.g., PAKCS
[
As already mentioned, the partial evaluator described in [
main = PEVAL (double coin)
w.r.t. the definitions of coin and double shown in Sect. 2. The partial evaluator [
The second missing feature are (mutually recursive) let expressions, i.e., bindings
where the variables to be bound might occur in the right-hand side of the bindings. For
example, it is not possible to partially evaluate the program
ones = let ones = 1 : ones in ones
main = PEVAL (take 2 ones)
One might encounter that this does not impose a real restriction because recursive
letbindings could be interpreted by recursive function definitions (at the cost of some
overhead). While this is possible for the example above, it is not whenever a
nondeterministic value should be shared. For instance, consider the following program:
digits = let digits = (0 ? 1) : digits in digits
main = PEVAL (take 2 digits)
Because of the let binding, the decision to bind digit to either 0 or 1 is shared, and, in
consequence, the expression main evaluates to either [0,0] or [
The usage of both features in contemporary Curry programs is the motivation for us
to develop a new partial evaluator. In contrast to [
FlatCurry is a simple intermediate language used by Curry compilers [
; z:zs → z : conc(zs,ys) }
Note that, in contrast to [
We base our partial evaluator on a variant of the operational semantics of FlatCurry
[
Heap = V → {free; ∎} ⊎ Exp
V alue ∶∶= x S c(xn) A heap is a partial mapping from a set of variables V to either an expression (Exp is the set of expressions according to the syntax of FlatCurry), a special symbol “free” to represent a free variable,1 or a symbol “∎” representing a black hole.2 We denote the empty heap by [], and the value associated to a variable x in a heap by [x]. [x ↦ e] denotes a heap ′ with ′[x] = e and ′[y] = [y] for all y ≠ x.
We use judgements of the form ∶ e ⇓ ∶ v which express the fact that “the
expression e under the heap evaluates to the value v and the (possibly modified) heap
”. The basic inference rules of the natural semantics are depicted in Fig. 3. We briefly
describe these rules and explain the differences to the original version of [
where ei ∉ V ; y fresh where f (xn) = e ∈ P;
= {xn ↦ yn} ∶ (e) ⇓ ∶ f (yn) ⇓ ∶ v ∶ v [yk ↦ (ek)] ∶ (e) ⇓ ∶ let { xk = ek } in e ⇓ ∶ v
∶ v ∶ ei ⇓ ∶ e1 ? e2 ⇓ ∶ v
∶ v [yn ↦ free] ∶ (e) ⇓ ∶ let xn free in e ⇓ ∶ v
∶ v where i ∈ {1; 2} where
= {xk ↦ yk}; yk fresh where
= {xn ↦ yn}; yn fresh ∶ e ⇓ ∶ c(yn) ∶ (ei) ⇓ ∶ case e of { pk → ek } ⇓ ∶ v ∶ v where pi = c(xn); = {xn ↦ yn} ∶ e ⇓ [x ↦ free] ∶ x [x ↦ (pi); yn ↦ free] ∶ (ei) ⇓
∶ case e of { pk → ek } ⇓ ∶ v
where i ∈ {1; : : : ; k}; pi = c(xn); = {xn ↦ yn}; yn fresh
∶ v
Following the general idea of partial evaluation of functional logic programs [
This residualizing natural semantics is similar to [
V alue ∶∶= : : : S ⟪e⟫ (annotated expression) This annotation directly corresponds to the PEVAL annotation in source programs. Second, we extend the inference system with the operation proceed , deciding whether a function call should be unfolded, and replace the rule Fun with:3 ∶ (e) ⇓ ∶ f (yn) ⇓ ∶ f (yn) ⇓ ∶ v ∶ v ∶ ⟪f (yn)⟫ where f (xn) = e ∈ P; = {xn ↦ yn};
proceed ( ; f (yn)) = true where f (xn) = e ∈ P; = {xn ↦ yn}; proceed ( ; f (yn)) = false Approaches for the concrete definition of proceed will be discussed in Sect. 5.1. Furthermore, we extend the rule Value to also return deferred expressions unchanged and constrain the rule VarExp in that the value must not be a deferred expression. Finally, we add two more rules for deferred expressions where the annotation is lifted upwards: In contrast to the evaluation performed in a standard interpreter, the partial evaluation process has to deal with partial knowledge in the form of unbound variables. For instance, if the right-hand side of a function declaration like f x = PEVAL (g x) should be evaluated, there is no binding information for the parameter variable x. 3 Actually, the operation proceed also takes into account the context of reductions already performed, but we omit them here for the sake of simplicity.
A possible solution is to handle such unbound variables as logic variables, as done
in [
let x free in case x of { True → 1 }
Here we can bind x to True, since this binding is not visible outside the scope of this
expression, select the (single) branch as the value of the case expression, and continue
by evaluating its right-hand side. In consequence, our implementation evaluates this
expression to 1, while the partial evaluator described in [
Hence, we distinguish unbound variables from logic variables by not binding them
in the heap. Furthermore, we assume that rule Value is also applicable to variables not
bound in the heap so that unknown variables reduce to themselves. Thus, only the rules
for case expressions have to be changed, where it is now also possible that the
scrutinized value is an unknown variable. Following the idea of [
V alue ∶∶= : : : S case x of { pk → vk } (residual case expression) where the variable x inspected in the case expression is not bound in the corresponding heap. Because case expressions are now contained in the set of values, we also have to consider them as the value of a variable or an expression examined by another case expression. Hence, we add the following rules: The general idea is to lift case expressions inspecting an unbound variable upwards and to defer the evaluation of the alternatives. Such deferred expressions are not further evaluated in the residual semantics but later extracted by the global iterative process where [x] = case y of { p′j → e′j } ∶ e ⇓ ∶ x
case x of ∶ case y of { p′j → ⟪ { pk → ek } ⟫ } as the initial expressions of a new specialization run. Because the alternatives are then evaluated independently, it will be possible to take the binding information of the case expression into account. For instance, if we consider the expression
case x of { True → not x } a subsequent evaluation of the right-hand side not x may respect the binding of x to True and, thus, directly evaluate to False. After evaluating an expression to a residual value, this value might contain variables which are either free or bound to expressions in the corresponding heap. To be able to replace parts of the input program with residual values, these bindings have to be added to the values to form valid expressions, a process we call dereferencing the heap. Conceptually, for a given configuration ∶ e, we retrieve the set of variables transitively reachable from e and bound in and add the corresponding bindings to the expression. For residual case expressions, we also respect the bindings represented by the case expression. The bindings are divided into logic variables (fv ) and variables bound to expressions (bv ) and added to the original expression: if e = case x of { pk → ek } otherwise ⎪⎧⎪case x of { pk → drf ( [x ↦ pk]; ek) } drf ( ; e) = ⎨⎪⎪⟪let fv ( ; e) free in let bv ( ; e) in e⟫
⎩ For instance, if we consider the configuration then dereferencing will produce the expression
[y ↦ free] ∶ case x of {True -> x; False -> y} case x of { True → ⟪let { x = True } in x⟫;False → ⟪let y free in y⟫ } 5
Our partial evaluation algorithm follows the general procedure of Alpuente et. al. [
i ∶= 0; E0 ∶= E; repeat
E′ ∶= unfold (Ei; P ); Ei+1 ∶= abstract (Ei; E′); i ∶= i + 1; until Ei = Ei+1 (modulo renaming); return S ∶= Ei
Fig. 4. Basic algorithm for partial evaluation
that covers all expressions possibly occurring in the residual program. To generate the
resulting program, the same unfolding rule has to be applied to the resulting set of
expressions to generate the corresponding resultants, i.e., the rules of the residual program
(in our implementation, this step is integrated into the algorithm). Finally, the set of
generated resultants are compressed to eliminate intermediate and redundant functions (see
[
This procedure distinguishes two levels of control, namely the local level, managed by the unfolding rule to avoid infinite evaluations, and the global level, managed by the abstraction operator to avoid infinitely repetitions of the partial evaluation algorithm. To ensure termination of the whole process, both local and global termination is required. 5.1
Termination of the unfolding rule directly corresponds to termination of the residual
semantics presented in Sect. 4. For this purpose, the semantics has already been extended
by an oracle proceed ( ; e) responsible for the decision whether a function call should
be unfolded or not. There exist several well-known techniques in the literature to come
to this decision, e. g., depth-bounds, loop-checks [
One Only one function call is unfolded for each evaluation.
Each At most one call is unfolded for each user-defined function, subsequent calls are deferred.
All All function calls are unfolded, which corresponds to the original inference system.
This does not guarantee termination but may be useful if the user is sure that the process terminates.
Note that, regardless of the chosen strategy, built-in functions (such as arithmetics) are evaluated in any case, since they are known to terminate.
Expressions that have been deferred during evaluation will be extracted and
eventually added to the set of expressions to be evaluated, depending on the operation abstract
(see Sect. 5.2 for details). Generally, a strategy that allows more evaluation steps in
one derivation than another strategy might seem superior. If an evaluation is split into
multiple derivations with deferred subexpressions, each of these subexpressions has to
be evaluated anew and leads to a new residual function to be generated. In contrast,
longer derivations will produce less deferred subexpressions and, hence, less residual
functions. Nevertheless, although a simpler strategy may produce more intermediate
expressions, there are better chances that some of these expressions have already been
encountered before, reducing the overall number of expressions to be evaluated.
Furthermore, the final compression phase will eliminate intermediate functions so that even
the simple strategies perform very well in practice.
The local control is parametric w.r.t. the decision whether to stop or to proceed with the
evaluation, since it is safe to terminate the evaluation at any point. This flexibility does
not apply to the global control because we cannot stop the iterative extension of the set
of expressions until all function calls in this set are “closed” w.r.t. the set of expressions.
An expression e is closed w.r.t. a set of expressions if it is an instance of an expression
in the set and all expressions in the matching substitution are recursively closed (see [
Hence, the operation abstract returns a safe approximation of Ei ∪ E′ so that each expression in the set of Ei ∪ E′ is closed w.r.t. the result of abstract (Ei; E′). More precisely, an expression e′ ∈ E′ is added to the set Ei according to the following rules (note that the result of unfolding is either a variable, a deferred expression, a constructor appplication, a case expression, or a choice of these results): 1. If e′ is a variable, it is discarded. 2. If e′ has the form ⟪e⟫, one of the following options is considered: (a) add e to the set Ei, (b) discard the expression e, or (c) compute the most specific generalization of e and some expression e′ ∈ E′, say e^, and try to add both e^ and the expressions in the corresponding substitutions and , where e = (e^) and e′ = (e^). 3. For all other cases (constructor calls, case expressions, choices), the corresponding subexpressions are considered.
Like for the unfolding rule, the abstraction can be parameterized by a criterion to decide the option taken in (2). Our implementation currently supports abstractions using a wellfounded ordering or an embedding ordering to distinguish between (2a) and (2c), i.e., smaller expressions are added but larger expressions are generalized.
To achieve a good level of specialization, it is crucial to recognize different variants
of one expression as equivalent in order to discard them in (2b). This is more
complex in our framework compared to [
In this section we evaluate the implementation of our partial evaluator by some benchmarks. We compile both the partial evaluator and the benchmarks with the PAKCS Curry compiler (version 1.11.3, based on SICStus Prolog 4.2.3). All benchmarks were executed on a Linux machine (Debian Wheezy) with an Intel Core i5-750 (2.66GHz) processor and 4GiB of memory. The timings were performed using the profiling operation profileTimeNF of PAKCS and denote the time required for computing the normal form of the respective result in milliseconds (the arguments passed to the various functions were evaluated before to bring out the speedup obtained by partial evaluation). The benchmark examples have been specialized with one unfolding per evaluation and without any abstraction, since all examples terminated. Experiments with both a wellfounded ordering or a well-quasi ordering resulted in the same or worse performance. Table 1 presents the time required for the partial evaluation process itself, for executing the original and the specialized program, and the gained speedup.
In the first group of benchmarks, we consider some typical examples of partial deduction and functional program transformations. These are simple functions working on lists or trees as (intermediate) data structures: allOnes computes the length of its input list, represented as Peano numbers, and constructs a new list of the same length with 1 as all elements, doubleApp is the concatenation of three lists, doubleFlip flips a tree structure twice, returning the same tree, lengthApp computes the length of the concatenation of two lists, and kmp implements a generic string pattern matcher. The first four functions were specialized without static input data, while the kmp example was specialized w.r.t. a fixed pattern of length 4, explaining both the time needed for partial evaluation and the gained speedup.
In the second group, we benchmark some examples with higher-order functions: the computation of the sum of list elements using foldr, the sum of squared numbers, the concatenation of a list of lists, and repeatedly applying a function to a list. All functions are applied to an input list xs containing 200,000 elements. The speedup is generally achieved because of the removal of intermediate data structures. For instance, the Curry expression “foldr (+) 0 (map square xs)” is specialized to the following residual FlatCurry definition: sumSquare(xs) = case xs of { [] → 0
; y:ys → (y*y) + sumSquare(ys) } Finally, we evaluate two (complicated) variants of the function choose, which nondeterministically chooses one element of a given list ys containing 10,000 elements: choose (x:xs) = x ? choose xs Our partial evaluator computes this simple implementation of choose for the first example. The result for the second example only differs from choose in the order in which the two non-deterministic alternatives are taken, which stems from the implementation of perm. The huge speedup is achieved because of the omission of the nondeterministic intermediate list structure.
To summarize, our partial evaluator shows promising results and is capable of
performing optimizations such as deforestation [
We have presented a new partial evaluation scheme for the functional logic language
Curry based on its intermediate representation FlatCurry. The partial evaluator is based
on an adaptation of the natural semantics of FlatCurry, extending the semantics to deal
with the requirements of partial evaluation such as ensuring termination. In contrast
to the original partial evaluator [
For future work, we intend to formally prove the correctness of the partial
evaluation scheme, which should be manageable due to the similarity of the original and
residual semantics. Another aspect for further investigations is the improvement of the
abstraction operator. While the abstraction is necessary to ensure termination, a too
general abstraction reduces the quality of the specialization. Thus, more sophisticated
abstraction operators might be beneficial.
As mentioned in Sect. 4.2, rule VarExp of the natural semantics shown in Fig. 3
replaces the variable binding x ↦ e by x ↦ ∎ in the heap when evaluating the associated
expression e. This allows the detection of black holes (a self-dependent infinite loop)
[
The detection of black holes included in the semantics seems to be an optimization
that could be omitted for deterministic programs [
∶ T ∶ x ⇓ [x ↦ T] ∶ T [x ↦ T] ∶ F ⇓ [x ↦ T] ∶ F
∶ case x of { T → F } ⇓ [x ↦ T] ∶ F ∶ T ? case x of { T → F } ⇓ [x ↦ T] ∶ F
∶ x ⇓ [x ↦ F] ∶ F [] ∶ let { x = T ? case x of { T → F } } in x ⇓ [x ↦ F] ∶ F where
= [x ↦ T ? case x of { T → F }] In this derivation, the variable x is looked up in the heap twice, where at first the right (non-deterministic) branch is chosen and afterwards the left branch. Hence, x is bound to T as well as F, which violates the single assignment property of call-time choice.
With our semantics, there is one successful and one failing derivation but no derivation where x is bound to T as well as F:
[x ↦ ∎] ∶ T ⇓ [x ↦ ∎] ∶ T [x ↦ ∎] ∶ T ? case x of { T → F } ⇓ [x ↦ ∎] ∶ T [x ↦ T ? case x of { T → F }] ∶ x ⇓ [x ↦ T] ∶ T [] ∶ let { x = T ? case x of { T → F } } in x ⇓ [x ↦ T] ∶ T
[x ↦ ∎] ∶ x ⇓ failure [x ↦ ∎] ∶ case x of { T → F } ⇓ [x ↦ ∎] ∶ T ? case x of { T → F } ⇓ [x ↦ T ? case x of { T → F }] ∶ x ⇓ [] ∶ let { x = T ? case x of { T → F } } in x ⇓ B
Since the various rules of the residualizing semantics used in our partial evaluator are distributed over the paper and some of them were only informally sketched, we summarize in the following the complete set of rules of our residualizing semantics. (VarDefer) (Flatten) (FunDefer) (Free) (Guess) (CaseUnbound) (CaseVarCase)
[x ↦ ∎] ∶ e ⇓ ∶ v [x ↦ e] ∶ x ⇓ [x ↦ v] ∶ v
[x ↦ ∎] ∶ e ⇓ ∶ ⟪e′⟫ [x ↦ e] ∶ x ⇓ [x ↦ e′] ∶ ⟪x⟫ where aen∉d{(fvre∈e;V∎o}r v = c(xn))
where e ∉ {free;∎} [x ↦ ∎] ∶ e ⇓ ∶ case y of{ pk → ⟪ek⟫ } [x ↦ e] ∶ x ⇓ [x ↦ case y of{ pk → ek }] ∶ x [y ↦ ei] ∶ (x1;:::;xi−1;y;ei+1;:::;ek) ⇓ ∶ v
∶ (x1;:::;xi−1;ei;ei+1;:::;ek) ⇓ ∶ v
where fpr(oxcnee)d=(e;∈fP(;yn)=){=xtnru↦e yn}; ∶ f(yn) ⇓ ∶ ⟪f(yn)⟫ where fpr(oxcnee)d=(e;∈fP(;yn)=){=xfnal↦seyn}; where e ∉ {free;∎}