Adding Data to Curry

Abstract

Functional logic languages can solve equations over user-defined data and functions. Thus, the definition of an appropriate meaning of equality has a long history in these languages, ranging from reflexive equality in early equational logic languages to strict equality in contemporary functional logic languages like Curry. With the introduction of type classes, where the equality operation “==” is overloaded and user-defined, the meaning became more complex. Moreover, logic variables appearing in equations require a different typing than pattern variables, since the latter might be instantiated with functional values or non-terminating operations. In this paper, we present a solution to these problems by introducing a new type class Data which is associated with specific algebraic data types, logic variables, and strict equality. We discuss the ideas of this class and its implications on various concepts of Curry, like unification, functional patterns, and program optimization.

1 Introduction

The amalgamation of the main declarative programming paradigms, namely functional and logic programming, has a long history. The advantages of such integrated functional logic languages are manifold. One can use the features of functional programming (e.g., powerful type systems, higher-order functions, lazy evaluation) and logic programming (e.g., non-deterministic search, computing with partial information) in a single language which also leads to new design patterns [3, 8]. Compared to logic programming, computations can be more efficient due to the use of optimal evaluation strategies [2].

Early approaches to integrating functional and logic programming (see [15] for a good collection of these proposals) used equational logic programming [19, 37] as a unifying framework. From a logic programming point of view, equational logic programming extends the meaning of the standard equality predicate “=” by taking user-defined functions into account before checking the equality of both sides of an equation. Hence, both sides are evaluated before they are unified. If the definition of evaluable functions are considered as axioms for an equational theory, this process is also known as E-unification [17]. In order to use logic programming techniques (computing with partial information) also for the evaluation of user-defined functions, one can use narrowing instead of reduction [40], i.e., replace pattern matching by unification when a function call should be reduced. In this way, functional logic languages based on narrowing can be used to solve equations.

Example 1

Consider the following definition of Peano numbers and their addition (in Haskell [39] syntax):

In the functional language Haskell, we can only compute the value of expressions, e.g.,

However, if we interpret these definitions as a program written in the (narrowing-based) functional logic language Curry [22, 27], we can also solve the equation

Here, “=:=” denotes equality w.r.t. user-defined operations (see below for more details) and x is declared as a free (logic) variable which is bound to S Z in order to evaluate the equation to True.

For the practical applicability of functional logic languages, it is important to reduce the computation space by using specific evaluation strategies. Thus, much work in this area has been devoted to develop appropriate narrowing strategies (see [21] for an early account of this research). In order to provide the advantages of lazy evaluation used in Haskell, e.g., optimal evaluation [29] and modularity [30], later research concentrated on demand-driven strategies. Needed narrowing [2] is an optimal strategy [1] and, thus, the basis of the language Curry.

Demand-driven evaluation strategies, like Haskell’s lazy evaluation or Curry’s needed narrowing, can deal with non-terminating operations that compute infinite data structures [30]. However, this could be in conflict with the equation solving capabilities of functional logic languages discussed above. Standard equality in the mathematical sense is required to be reflexive, i.e., $x = x$ should always hold [37]. Now consider two operations to compute infinite lists of Peano numbers:

By reflexivity, $\texttt {f1}\,\texttt {Z} = \texttt {f1}\,\texttt {Z}$ should hold. This means that the infinite lists of all Peano numbers are equal. As a consequence, $\texttt {f1}\,\texttt {Z} = \texttt {f2}\,\texttt {Z}$ should also hold, but it is unclear to verify it during run time. In early equational logic programming, equations are solved by narrowing both sides to normal forms and unifying these normal forms. However, this does not work here since f1 Z and f1 Z have no normal form. Thus, reflexivity is not a feasible property of equations to be evaluated (more details including issues about semantics are discussed in [18, 36]).

Therefore, contemporary languages interpret equations to be evaluated as strict equality, denoted by “=:=” in Curry: $e_1\,{\texttt {=:=}}\,e_2$ is satisfied iff $e_1$ and $e_2$ are reducible to a same ground constructor term, i.e., an expression without variables and defined functions. In particular, soundness, completeness, and optimality results are stated w.r.t. strict equality [2]. As a consequence, f1 Z =:= f1 Z does not hold so that it is not a defect that this equation cannot be solved.

Note that Haskell also offers the operation “==” intended to compare expressions. Although standard textbooks on Haskell define this operation as “equality” [11, 31, 41], its actual implementation can be different since, as a member of the type class Eq, it can be defined with a behavior different than equality on concrete type instances. Actually, the documentation of the type class Eq¹ denotes “==” as “equality” but also contains the remark: “== is customarily expected to implement an equivalence relationship where two values comparing equal are indistinguishable by “public” functions.” Thus, it is intended that $e_1\,{\texttt {==}}\,e_2$ evaluates to True even if $e_1$ and $e_2$ have not the same but only equivalent values. On the other hand, the documentation requires that the reflexivity property

holds for any implementation, but this is not true even for the standard integer equality (choose for x).

This discussion shows that the precise treatment of equality, which is essential for functional logic languages, might have some pitfalls when type classes are used. As long as “==” is defined in the standard way (by the use of “deriving Eq”), “==” conforms with strict equality. With the introduction of type classes to Curry, one has to be more careful. For instance, consider the “classical” functional logic definition of the operation last to compute the last element of a list by exploiting list concatenation (“++”) and equation solving [21, 24]:

If “==” denotes equivalence rather than strict equality, last might not return the last element of a list but one (or more than one) value which is equivalent to the last element.

In this paper, we propose a solution to these problems by distinguishing between strict equality and equivalence. For this purpose, we propose a new type class Data which is associated with specific algebraic data types. We will see that this type class can also be used for a better characterization of the meaning of logic variables and the Curry’s unification operator “=:=”.

This paper is structured as follows. In the next section, we review some aspects of functional logic programming and Curry. After motivating the problem this paper tackles in Sect. 3, we propose in Sect. 4 a new standard type class for Curry, namely Data, as a solution to the problem. In Sects. 5, 6, and Sect. 7, we discuss how the proposed Data type class affects logic variables, optimization of equality constraints, and non-left-linear rules and functional patterns, respectively. Finally, Sect. 8 discusses related work before we conclude in Sect. 9.

2 Functional Logic Programming and Curry

We briefly review some aspects of functional logic programming and Curry that are necessary to understand the contents of this paper. More details can be found in surveys on functional logic programming [7, 24] and in the language report [27].

Curry is a declarative multi-paradigm language intended to combine the most important features from functional and logic programming. The syntax of Curry is close to Haskell [39] but also allows free (logic) variables in conditions and right-hand sides of rules. Thus, expressions in Curry programs contain operations (defined functions), constructors (introduced in data type declarations), and variables (arguments of operations or free variables). Function calls with free variables are evaluated by a possibly non-deterministic instantiation of demanded arguments [2]. This corresponds to narrowing [40], but Curry narrows with possibly non-most-general unifiers to ensure the optimality of computations [2]. In contrast to Haskell, rules with overlapping left-hand sides are non-deterministically (rather than sequentially) applied.

Example 2

The following simple program shows the functional and logic features of Curry. It defines the well-known list concatenation and an operation that returns some element of a list having at least two occurrences:

Since “++” can be called with free variables in arguments, the condition in the rule of someDup is solved by instantiating x and the anonymous free variables to appropriate values before reducing the function calls. As already mentioned in the introduction, “=:=” denotes strict equality, i.e., the condition of someDup is satisfied if both sides are reduced to a same ground constructor term. In order to avoid the enumeration of useless values, “=:=” is implemented as unification: if y and z are free (unbound) variables, ${\texttt {{y}\,{=:=}\,{z}}}$ is evaluated (to True) by binding y and z (or vice versa) instead of non-deterministically binding y and z to identical ground constructor terms. This can be interpreted as an optimized implementation by delaying the bindings to ground constructor terms [10]. Due to this implementation, “=:=” is also called an equational constraint (rather than Boolean equality).

We already used the logic programming features of Curry in the definition of last shown in Sect. 1. In contrast to last, someDup is a non-deterministic operation since it could yield more than one result for a given argument, e.g., the evaluation of someDup [1,2,2,1] yields the values 1 and 2. Non-deterministic operations, which can formally be interpreted as mappings from values into sets of values [20], are an important feature of contemporary functional logic languages. Hence, Curry has also a predefined choice operation:

Thus, the expression “0 ? 1” evaluates to 0 and 1 with the value non-deterministically chosen.

3 Equality vs. Equivalence

Type classes are an important feature to express ad-hoc polymorphism in a structured manner [42]. In the context of Curry, it is also useful to restrict the application of some operations to unintended expressions. For instance, in the definition of Curry without type classes [27], the type of the unification operator is defined as

This implies that we could unify values of any type, including defined functions. However, the meaning of equality on functions is not well defined. The Curry implementation PAKCS [26], which compiles Curry programs into Prolog programs, uses an intensional meaning, i.e., functions are equal if they have the same name. This means that PAKCS evaluates

to True but it fails on

(since the lambda abstraction will be lifted into a new top-level function). Moreover, the Curry implementation KiCS2 [12], which compiles Curry programs into Haskell programs, produces an internal error for these expressions.

It would be preferable to forbid the application of “=:=” to functional values at compile time. This is similar to the requirement on Haskell’s operator “==”. Haskell uses the type class Eq in order to express that “==” is not parametric polymorphic but overloaded for some (but not all) types. The type class Eq contains two operations (we omit the default implementations):

Hence, the operator “==” cannot be applied to any type but only to types defining instances of this class. We can use this operator to check whether an element occurs in a list:

Although type classes express type restrictions in an elegant manner, they might also cause unexpected behaviors if they are not carefully used. For instance, we can define a data type for values indexed by a unique number:

Since the index is assumed to be unique, we define the comparison of index values by just comparing the indices:

With this definition, the operation elem defined above could yield surprising results:

This is not intended since the element (first argument) does not occur in the list. Actually, the Haskell documentation² about elem contains the explanation “Does the element occur in the structure?” which ignores the fact that some instances of Eq are only equivalences rather than identities.

This unusual behavior could also influence logic-oriented computations in a surprising manner. If the operation last is defined as shown in Sect. 1, we obtain the following answer when computing the last element of a given IVal list (here, denotes a logical variable of type Char):

Hence, instead of the last element, we get a rather general representation of it.

The next section presents our proposal to solve these problems.

4 Data

As discussed above, type classes are an elegant way to express type restrictions. On the other hand, it is not a good idea to allow user-defined instance definitions of important operations like strict equality. Therefore, we propose the introduction of a specific type class where only standard instances can be derived so that all instances satisfy the intended meaning. This type class is called Data and has the following definition:

Thus, any instance of this class provides two operations:

• The non-deterministic operation aValue returns some value, i.e., the complete evaluation of aValue yields all values of type a.

• The operation “===” implements the standard equality on values, i.e., it returns True or False depending on whether the argument values are identical or not.

The following definition specifies how to automatically derive a Data instance for any algebraic datatype.

Definition 1

If T is an algebraic datatype declared by

the standard derived Data instance has the following form:

In the instance declaration above, the context cx consists of Data constraints ensuring that Data $b_{ij}$ holds for each type $b_{ij}$ with $i \in \{1, \ldots , n\}$ and $j \in \{1, \ldots , k_i\}$.

Example 3

For the type of Peano numbers (see Example 1), the Data instance can be defined as follows:

A Data instance for lists requires a Data instance for its elements:

The operation aValue is useful when a value of some data type should be guessed, e.g., for testing [25]. The obvious relation to logic variables will be discussed later.

The definition of “===” is identical to “==” if the definition of the latter is automatically derived (by a “deriving Eq” clause). As discussed above, it is also possible to define other instances of Eq that leads to unintended results. To ensure that “===” always denotes equality on values, it is not allowed to define explicit Data instances as shown above. Such instances can only be generated by adding a “deriving Data” clause to a data definition. Note that an instance derivation requires that all arguments of all data constructors have Data instances. In particular, if some argument has a functional type, e.g.,

then a Data instance can not be derived.

For ease of use, one could always derive Data instances for data declarations whenever it is possible (i.e., functional values do not occur in arguments), or provide a language option to turn this behavior on or off.

With the introduction of the class Data, we can specify a more precise type to Curry’s strict equality operation “=:=”. As discussed in [10], the meaning of “=:=” is the “positive” part of “===”, i.e., its semantics can be defined by

$$\begin{aligned} \texttt {x =:= y ~=~ solve}\,\texttt {(x === y)} \end{aligned}$$

(1)

where solve is an operator that enforces positive evaluations for Boolean expressions:

$$\begin{aligned} \texttt {solve}\,\texttt {True = True} \end{aligned}$$

(2)

Since expressions of the form $e_1\,{\texttt {=:=}}\,e_2$ might return True but never False, “=:=” can be implemented by unification, as already discussed in Sect. 2. Such an optimized implementation is justified by the definition (1) above. However, if the semantics of “=:=” is defined by

$$\begin{aligned} \texttt {x =:= y ~=~ solve}\,\texttt {(x == y)} \end{aligned}$$

(3)

as suggested before the introduction of type classes to Curry [9], an implementation of “=:=” by unification would not be correct since unification might put stronger requirements on expressions to be compared than actually defined by Eq instances.

As a spin-off of definition (1), we obtain a more restricted type of “=:=”:

(4)

This avoids the problems with the application of “=:=” to functional values sketched at the beginning of Sect. 3.

5 Logic Variables

When a function call with free variables in arguments is evaluated by narrowing, the free variables are instantiated to values so that the function call becomes reducible. Conceptually, a free variable denotes possible values so that a computation can pick one in order to proceed. With the definition of the type class Data and the non-deterministic operation aValue, we make the notion of “possible value” explicit. Actually, it has been shown that non-deterministic operations and logic variables have the same expressive power [5, 14] since one can replace logic variables occurring in a functional logic program by non-deterministic value generators.

Example 4

Consider the addition on Peano numbers shown in Example 1 which is exploited to define subtraction:

We can replace the logic variable z by a value generator:

The equivalence of logic variables and non-deterministic value generators can be exploited when Curry is implemented by translation into a target language without support for non-determinism and logic variables. For instance, KiCS2 [12] compiles Curry into Haskell by adding only a mechanism to handle non-deterministic computations. Therefore, KiCS2 is able to evaluate a logic variable to all its values. Thus, KiCS2 could exploit this fact by using the following alternative definition for aValue:

(5)

This equivalence also sheds some new light on the type of logic variables. Currently, logic variables without any constraints on their types are considered to have a polymorphic type. For instance, the inferred type of aValue as defined in (5) is

However, this type does not really describe the intent of this operation, since aValue does not yield functional values. For instance, consider the definition

The type currently inferred is

However, it is meaningless to use the result of some application of f in contexts where a function is required. For instance, the evaluation of the expression

$$\begin{aligned} \texttt {map}\,\texttt {(f}\,\texttt {True)}\,\texttt {[0,1]} \end{aligned}$$

(6)

suspends in PAKCS and produces a run-time error in KiCS2 (very similar to the examples described at the beginning of Sect. 3). Furthermore, the inferred type of the definition

is

Thus, it looks very similar to the type of f although g has a quite different meaning: in contrast to f, an application of g never returns a value.

All these problems can be avoided by a simple fix: logic variables are considered as equivalent to the operation aValue of type class Data so that a logic variable without any constraints on its type has type a where a is constrained with the type class context Data a. With this change, the inferred type of f is

As a consequence, expression (6) will be rejected by the type checker since functions have no Data instance.

6 Equality Optimization

Choosing the appropriate kind of equality might not be obvious to the programmer. The difference between identity and equivalence is semantically relevant so that the decision between “===” and “==” is not avoidable. However, “=:=” can be considered as an optimization of “===” so that it is not obvious when it should be applied. In order to simplify this situation, it has been argued in [9, 10] that the programmer should always use strict equality (i.e., “===”) and the selection of “=:=” should be done by an optimization tool. This tool analyzes the required values of Boolean expressions. If an application of strict equality requires only the result value True, e.g., in guards of conditional rules or in arguments of solve, see (2), then one can safely replace the equality operator by the unification operator “=:=” (see [10] for details). For instance, if last is defined by

then it can be transformed into

As shown in [10], this transformation can have a big impact on the execution time.

Up to now, this tool (which is part of the compilation chain of Curry systems) considered the optimization of calls to “==”. Since this might lead to incompleteness, as discussed above, it has to consider calls to “===” when the type class Data is introduced. However, for backward compatibility and better optimizations, one can extend the optimizer also to calls of the form $e_1\,{\texttt {==}}\,e_2$: if the types of the arguments $e_1,e_2$ are monomorphic and the Eq instances of these types are derived with the default scheme (by deriving annotations), the semantics of “==” is identical to the semantics of “===” so that one can replace $e_1\,{\texttt {==}}\,e_2$ by $e_1\,{\texttt {===}}\,e_2$ and apply the optimization sketched above.

7 Non-left-Linear Rules and Functional Patterns

The proposed introduction of the type class Data together with the adjusted type of the unification operator “=:=” has also some influence on language constructs where unification is implicitly used. We discuss this in more detail in this section.

In contrast to Haskell, Curry allows non-left-linear rules, i.e., defining rules with multiple occurrences of a variable in the patterns of the left-hand side. For instance, this function definition is valid in Curry:

Multiple occurrences of variables in the left-hand side are considered as an abbreviation for equational constraints between these occurrences [27], i.e., the definition above is expanded to

This feature of Curry is motivated by logic programming where multiple variable occurrences in rule heads are also solved by unification. However, in Curry the situation is a bit more complex due to the inclusion of functions and infinite data structures. As a matter of fact, our refined type of “=:=” makes the status of non-left-linear rules clearer. According to the type shown in (4), the type inferred for the definition above is

Hence, f can not be called with functional values as arguments. This even increases the compatibility with logic programming where unification is applied to Herbrand terms, i.e., algebraic data.

Another feature of Curry, where equational constraints are implicitly used, are functional patterns. Functional patterns are proposed in [4] as an elegant way to describe pattern matching with an infinite set of patterns. For instance, consider the definition of last shown above. Since the equational condition requires the complete evaluation of the input list, an expression like last [failed,3] (where failed is an expression that has no value) can not be evaluated to some value. Now, consider that last is defined by the following (infinite) set of rules:

Then the expression above is reduced to the value 3 by applying the second rule. This set of rules can be abbreviated by a single rule:

(7)

Since the argument contains the defined operation “++”, it is called a functional pattern. Conceptually, a functional pattern denotes all constructor terms to which it can be evaluated (by narrowing). In this case, these are the patterns shown above. Operationally, pattern matching with functional patterns can be implemented by a specific unification procedure which evaluates the functional pattern in a demand-driven manner [4]. Functional patterns are useful to express pattern matching at arbitrary depths in a compact manner. For instance, they can be exploited for a compact and declarative approach to process XML documents [23].

A delicate point of functional patterns are non-linear patterns, i.e., if a functional pattern is evaluated to some constructor term containing multiple occurrences of a variable. For instance, consider the function

and its use in a functional pattern:

By the semantics of functional patterns, the latter rule is equivalent to the definition

Due to the non-linear left-hand side, the type of whenDup is

Now, consider the operation const defined by

and its use in a functional pattern:

$$\begin{aligned} \texttt {g}\,\texttt {(const}\,\texttt {x}\,\texttt {x)} = \texttt {x} \end{aligned}$$

(8)

By the semantics of functional pattern, the definition of g is equivalent to

so that a correct type is

Hence, the type context Data a is not required, although the variable x has a multiple occurrence in (8). This example shows that, if functional patterns are used, the requirement for a Data context depends on the linearity of the constructor terms to which the functional patterns evaluate. Since this property is undecidable in general, a safe approximation is to add a Data constraint to the result type of the functional pattern. This has the consequence that the type of last, when defined as in (7), is inferred as

Basically, this type is the same as we would obtain when defining last with an equational constraint, but it could be done better: since the functional pattern always yields a linear term, the type class constraint Data a is not necessary. Hence, one can make the type checking for operations defined with functional patterns more powerful by approximating the linearity property of the functional pattern. Such an approximation has already been used in [4] to improve the efficiency of the unification procedure for functional patterns. However, a significant drawback would be the fact that the inferred type of a function would depend on the quality of the approximation. As a consequence, the principal type of a function [13, 28] would become ambiguous under certain circumstances and would depend on a function’s implementation.

8 Related Work

We already discussed in the previous sections some work related to the interpretation and use of equality in declarative languages. In the following, we focus on some additional work related to our proposal.

The necessity to distinguish different equalities in the context of functional logic programming and to define their exact semantics has been recognized before. In [16], the authors introduce several equality (and disequality) operations, among others also an operation for strict equality. However, no explicit distinction between equality and equivalence is made as only the former is discussed. Note also that some of these operations became obsolete with [9].

In [33], the author discusses the addition of Haskell-like overloading to Curry. In doing so, a new type class Equal that contains the unification operation “=:=” is proposed. The intent is to restrict this operation similarly to the equivalence operation “==” so that it is only applicable to certain types. In contrast to our proposal, it is not enforced that instances of the Equal type class should always have the same form. In the same work, another type class Narrowable containing a method called narrow is proposed in order to restrict the type of logical variables against the background of higher-rank types. The method narrow is very similar to our method aValue. But aside from a few downsides of the introduction of such a method, e.g., a possibly fixed order when enumerating solutions, no further consequences for the language itself are discussed in that work.

The idea to use a type relation to restrict the type of logical variables has also been introduced in [35] for a better characterization of free theorems. In [34], a type class Data is used for the same reason, but the class is only used as a marker (as in [35]) so that the type class does not contain any methods.

On a side note, there is also a Data type class in Haskell. However, this particular type class is used for generic programming in Haskell and shares nothing but the name with our type class [32].

9 Conclusions

In this paper we presented a solution to various problems w.r.t. equality and logic variables in functional logic programs by introducing a new type class Data. Instances of this class support a generator operation aValue for values and a strict equality operation “===” on these values. In contrast to other classes, instances of this class can only be derived in a standard manner and cannot be defined by the programmer. This decision ensures a reasonable semantics: if $e_1\,{\texttt {===}}\,e_2$ evaluates to True, then the expressions $e_1$ and $e_2$ have an identical value. Although this is the notion of strict equality proposed for a long time, Haskell-like overloading of the class Eq and its operation “==” allows to specify that “some expressions are more equal than others” [38].

At a first glance, it might be unnecessary to add a further equality operator and base type class to a declarative language. The advantage is that this supports a clear documentation for all functions depending on equality, as it makes a huge difference in functional logic programming whether one imposes equality or equivalence in a function’s implementation. If a programmer is interested in identical values, she or he has to use “===”.³ If only equivalence is relevant, “==” is the right choice. For instance, consider the operation elem to check whether an element occurs in a list. The type

indicates that this operation succeeds if the element actually occurs in the list, whereas the type

indicates that it succeeds if some equivalent element is contained in the list.

Unfortunately, these details are often not taken into account. As discussed in this paper, many textbooks and program documentations simply ignore such differences or are not formally precise in their statements.

We showed that our proposal is also useful to type logic variables in a more meaningful way. The type of a logic variable is required to be an instance of Data so that one can enumerate the possible values of this variable. Although logic variables are often instantiated by narrowing or unification to appropriate values, there are situations where an explicit enumeration is necessary to ensure completeness. For instance, consider the encapsulation of non-deterministic computations in order to reason about the various outcomes. Set functions [6] are a declarative, i.e., evaluation-independent, encapsulation approach. If f is a (unary) function, its set function $f_\mathcal{S}$ returns the set of all results computed by f for a given argument. For instance, returns the set of all duplicate elements (see Example 2) occurring in the list xs. An important property of a set function is that it encapsulates only the non-determinism caused by the function’s definition and not by the arguments. Hence, yields two different sets: $\{\texttt {1}\}$ and $\{\}$. This property of set functions is important to ensure their declarative semantics. It has the consequence that arguments must be evaluated outside the set function. Hence, to evaluate the expression

it is not allowed to bind x inside the evaluation of f. As a consequence, x must be instantiated outside in order to proceed a computation where f demands its argument. This can easily be obtained by the use of the operation aValue:

In order to evaluate the practical consequences of our proposal, we implemented it in a prototypical manner in our Curry front end that is used by various Curry implementations. The changes in the type checker were minimal (e.g., adding Data contexts to the inferred types of logic variables). Concerning libraries, only a single type signature had to be adapted in the standard prelude, one of the largest Curry modules: the type of the “arbitrary value” operation gets a Data context:

In other libraries, only a few types (related to search encapsulation primitives) had to be adapted. With these few changes, even larger Curry applications could be compiled without problems. This demonstrates that our proposal is a viable alternative to the current unsatisfying handling of equality and logic variables in Curry. Usually, no changes are necessary in existing Curry programs. Only in the rare cases of function definitions with polymorphic non-linear left-hand sides or polymorphic logic variables, type signatures have to be adapted.