Curry

An Integrated Functional Logic Language

Draft of February 2, 1998

Michael Hanus^{1} [editor]

Additional Contributors:

Sergio Antoy^{2} Herbert Kuchen^{3}

Francisco J. López-Fraguas^{4} Frank Steiner^{5}

(1) RWTH Aachen, Germany, hanus@informatik.rwth-aachen.de

(2) Portland State University, USA, antoy@cs.pdx.edu (3) University of Münster, Germany, kuchen@uni-muenster.de

(4) UCM Madrid, Spain, fraguas@dia.ucm.es

(5) RWTH Aachen, Germany, fufu@i2.informatik.rwth-aachen.de

Contents

1 Introduction 3

2 Programs 3 2.1 Datatype Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Function Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3 Local Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.4 Free Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.5 Constraints and Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.6 Higher-order Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

3 Operational Semantics 9

4 Types 11 4.1 Built-in Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4.2 Type System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

5 Modules 15

6 Input/Output 19

7 Encapsulated Search 20 7.1 Search Goals and Search Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 7.2 Local Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 7.3 Predefined Search Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 7.4 Choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

8 Interface to External Functions and Constraint Solvers 25 8.1 External Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 8.2 External Constraint Solvers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

9 Pragmas 26

10 Interactive Programming Environment 27

A Example Programs 28 A.1 Operations on Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 A.2 Higher-Order Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 A.3 Relational Programming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 A.4 Constraint Solving and Concurrent Programming . . . . . . . . . . . . . . . . . . . . 31 A.5 Concurrent Object-Oriented Programming . . . . . . . . . . . . . . . . . . . . . . . . 33

B Standard Prelude 35 C Syntax of Curry 40

C.1 Lexicon . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 C.2 Layout . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 C.3 Context Free Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41

D Operational Semantics of Curry 44 D.1 Definitional Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 D.2 Computation Steps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 D.3 Conditional Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 D.4 Equational Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 D.5 Higher-Order Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 D.6 Generating Definitional Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 D.7 Encapsulated Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

Bibliography 53

Index 57

1 Introduction

Curry is a universal programming language aiming at the amalgamation of the most important declarative programming paradigms, namely functional programming and logic programming. Curry combines in a seamless way features from functional programming (nested expressions, lazy evaluation, higher-order functions), logic programming (logical variables, partial data structures, built-in search), and concurrent programming (concurrent evaluation of constraints with synchronization on logical variables). Moreover, Curry provides additional features in comparison to the pure languages (compared to functional programming: search, computing with partial information; compared to logic programming: more efficient evaluation due to the deterministic evaluation of functions). Moreover, it also amalgamates the most important operational principles developed in the area of integrated functional logic languages: “residuation” and “narrowing” (see [19] for a survey on functional logic programming).

The development of Curry is an international initiative intended to provide a common platform for the research, teaching^{1} and application of integrated functional logic languages. This document describes the basic features of Curry.

2 Programs

A Curry program specifies the semantics of expressions, where goals, which occur in logic programming, are particular Boolean expressions. Executing a Curry program means simplifying an expression until a value (or solution) is computed. To distinguish between values and reducible expressions, Curry has a strict distinction between (data) constructors and and operations or defined functions on these data. Hence, a Curry program consists of a set of type and function declarations. The type declarations define the computational domains (constructors) and the function declarations the operations on these domains. Predicates are considered as Boolean functions.

Modern functional languages (e.g., Haskell [25], SML [33]) allow the detection of many programming errors at compile time by the use of polymorphic type systems. Similar type systems are also used in modern logic languages (e.g., Gödel [24], λProlog [35]). Therefore, Curry is a strongly typed language with a Hindley/Milner-like polymorphic type system [13].^{2} Each object in a program has a unique type, where the types of variables and operations can be omitted and are reconstructed by a type inference mechanism.

2.1 Datatype Declarations

A datatype declaration has the form

data T α_{1} ... α_{n} = C_{1} τ_{11} ... τ_{1n_{1}} | ⋯ | C_{k} τ_{k1} ... τ_{kn_{k}}

and introduces a new n-ary type constructor T and k new (data) constructors C_{1}, …, C_{k}, where each C_{i} has the type

1Actually, Curry has been successfully applied to teach functional and logic programming techniques in a single course without switching between different programming languages. More details about this aspect can be found in [20].

2The extension of this type system to Haskell’s type classes is not included in the kernel language but will be considered in a future version.

τ_{i1} -> ⋯ -> τ_{in_{i}} -> T α_{1} … α_{n}

(i = 1, …, k). Each τ_{ij} is a type expression built from the type variables α_{1}, …, α_{n} and some type constructors. Curry has a number of built-in type constructors, like Bool, Int, -> (function space), or, lists and tuples, which are described in Section 4.1. Since Curry is a higher-order language, the types of functions (i.e., constructors or operations) are written in their curried form τ_{1} -> τ_{2} -> ⋯ -> τ_{n} -> τ where τ is not a functional type. In this case, n is called the arity of the function. For instance, the datatype declarations

     data Bool = True | False
     data List a = [] | a : List a
     data Tree a = Leaf a | Node (Tree a) a (Tree a)

introduces the datatype Bool with the 0-ary constructors (constants) True and False, and the polymorphic types List a and Tree a of lists and binary trees. Here, “:” is an infix operator, i.e., “a:List a” is another notation for “(:) a (List a)”. Lists are predefined in Curry, where the notation “[a]” is used to denote list types (instead of “List a”). The usual convenient notations for lists are supported, i.e., [0,1,2] is an abbreviation for 0:(1:(2:[])) (see also Section 4.1).

A data term is a variable x or a constructor application c t_{1} … t_{n} where c is an n-ary constructor and t_{1}, …, t_{n} are data terms. An expression is a variable or a (partial) application φ e_{1} … e_{m} where φ is an n-ary function or constructor, m ≤ n, and e_{1}, …, e_{m} are expressions. A data term or expression is called ground if it does not contain any variable. Ground data terms correspond to values in the intended domain, and expressions containing operations should be evaluated to data terms. Note that traditional functional languages compute on ground expressions, whereas logic languages also allow non-ground expressions.

2.2 Function Declarations

A function is defined by a type declaration (which can be omitted) followed by a list of defining equations. A type declaration for an n-ary function has the form

f :: τ_{1} -> τ_{2} -> ⋯ -> τ_{n} -> τ

where τ_{1}, …, τ_{n}, τ are type expressions and τ is not a functional type. The simplest form of a defining equation (or rule) for an n-ary function f (n ≥ 0) is

f t_{1} … t_{n} = e

where t_{1}, …, t_{n} are data terms and the right-hand side e is an expression. The left-hand side f t_{1} … t_{n} must not contain multiple occurrences of a variable. Functions can also be defined by conditional equations which have the form

f t_{1} … t_{n} | {c} = e

where the condition c is a constraint (cf. Section 2.5). In order to apply a conditional equation, its condition must be solved. For convenience one can also write conditional equations in the Haskell-like notation

f t_{1} … t_{n} | b = e

(where b is an expression of type Bool) which is considered as an abbreviation for the rule

f t_{1} … t_{n} | {b=True} = e

Note that one can define functions with a non-determinate behavior by providing several rules with overlapping left-hand sides or free variables (i.e., variables which do not occur in the left-hand side) in the conditions or right-hand sides of rules. For instance, the following non-deterministic function inserts an element at an arbitrary position in a list:

     insert x []     = [x]
     insert x (y:ys) = x : y : ys
     insert x (y:ys) = y : insert x ys

Such non-deterministic functions can be given a perfect declarative semantics [17] and their implementation causes no overhead in Curry since techniques for handling non-determinism are already contained in the logic programming part (see also [4]). However, deterministic functions are advantageous since they provide for more efficient implementations (like the dynamic cut [31]). If one is interested only in defining deterministic functions, this can be ensured by the following restrictions:

1. Each variable occurring in the right-hand side of a rule must also occur in the corresponding left-hand side.

2. If f t_{1} … t_{n} | {c} = e and f t′_{1} … t′_{n} | {c′} = e′ are rules defining f and σ is a substitution^{3} with σ(t_{1} … t_{n}) = σ(t′_{1} … t′_{n}), then at least one of the following conditions holds:

(a) σ(e) = σ(e′) (compatibility of right-hand sides).

(b) σ(c) and σ(c′) are not simultaneously satisfiable (incompatibility of conditions). A decidable approximation of this condition can be found in [27].

These conditions ensure the confluence of the rules if they are considered as a conditional term rewriting system [44]. Implementations of Curry may check these conditions and warn the user if they are not satisfied. There are also more general conditions to ensure confluence [44] which can be checked instead of the above conditions.

Note that defining equations of higher-type, e.g., f = g if f and g are of type Bool -> Bool, are formally excluded in order to define a simple operational semantics based on first-order rewriting.^{4} Therefore, a defining equation f = g between functions will be interpreted in Curry as syntactic sugar for the corresponding defining equation f x = g x on base types.

2.3 Local Declarations

Since not all auxiliary functions and values should be globally visible, it is possible to restrict the scope of declared entities. Note that the scope of parameters in function definitions is already restricted since the variables occurring in parameters of the left-hand side are only visible in the corresponding conditions and right-hand sides. The visibility of other entities can be restricted using let in expressions or where in defining equations.

3A substitution σ is a mapping from variables into expressions which is extended to a homomorphism on expressions by defining σ(f t_{1} … t_{n}) = f σ(t_{1}) … σ(t_{n}). {x_{1} = e_{1}, …, x_{k} = e_{k}} denotes the substitution σ with σ(x_{i}) = e_{i} (i = 1, …, k) and σ(x) = x for all variables x ∉ {x_{1}, …, x_{k}}.

4Note that this is also necessary in an extension of Curry which allows higher-order rewrite rules, since rules with lambda-abstractions in left-hand sides which are not of base type may cause a gap between the standard notion of higher-order rewriting and the corresponding equational theory [38].

An expression of the form let decls in exp introduces a set of local values. The list of local declarations decls can contain function definitions as well as definitions of constants by pattern matching. The names introduced in these declarations are visible in the expression exp and the right-hand sides of the declarations in decls, i.e., the local declarations can be mutually recursive. For instance, the expression

     let a=3*b
         b=6
     in 4*a

reduces to the value 72.

Auxiliary functions which are only introduced to define another function should often not be visible outside. Therefore, such functions can be declared in a where-clause added to the righthand side of the corresponding function definition. This is done in the following definition of a fast exponentiation where the auxiliary functions even and square are only visible in the right-hand side of the rule for exp:

     exp b n = if n==0
               then 1
               else if even n then square (exp b (n `div` 2))
                              else b * (exp b (n-1))
            where even n = n `mod` 2 == 0
                  square n = n*n

Similarly to let, where-clauses can contain mutually recursive function definitions as well as definitions of constants by pattern matching. The names declared in the where-clauses are only visible in the corresponding conditions and right-hand sides. As a further example, the following Curry program implements the quicksort algorithm with a function split which splits a list into two lists containing the smaller and larger elements:

     split e []            = ([],[])
     split e (x:xs) | e>=x = (x:l,r)
                    | e<x  = (l,x:r)
                    where
                      (l,r) = split e xs
     qsort []     = []
     qsort (x:xs) = qsort l ++ (x:qsort r)
                  where
                    (l,r) = split x xs

2.4 Free Variables

Since Curry is intended to cover functional as well as logic programming paradigms, expressions (or constraints, see Section 2.5) might contain free (unbound, uninstantiated) variables. The idea is to compute values for these variables such that the expression is reducible to a data term or that the constraint is solvable. For instance, consider the definitions

     mother John    = Christine
     mother Alice   = Christine
     mother Andrew  = Alice

Then we can compute a child of Alice by solving the equation (see Section 2.5) mother x = Alice. Here, x is a free variable which is instantiated to Andrew in order to reduce the equation’s lefthand side to Alice. Similarly, we can compute a grandchild of Chistine by solving the equation

mother (mother x) = Christine which yields the value Andrew for x.

In logic programming languages like Prolog, all free variables are considered as existentially quantified at the top-level. Thus, they are always implicitly declared at the top-level. In a language with different nested scopes like Curry, it is advantageous to declare the variables in the scope where they occur (this becomes important in the presence of search operators or committed choice, see Section 7). Thus, each free variable x should be explicitly declared using a declaration of the form x free. These declarations can occur in where-clauses or in a let enclosing a constraint. The variable is then introduced as unbound with the same scoping rules as for all other local entities (see Section 2.3). For instance, we can define

     isgrandmother g | let c free in {mother (mother c) = g} = True

As a further example, consider the definition of the concatentation of two lists:

     append []     ys = ys
     append (x:xs) ys = x : append xs ys

Then we can define the function last which computes the last element of a list by the rule

     last l | let xs free in {append(xs,[x])=l} = x  where x free

In order to provide a convenient logic programming style with implicit declarations, variables starting with an underscore are treated as free variables, where _denotes an anonymous variable which is interpreted as a different variable at each occurrence. Thus, we can write the last rule also in the following equivalent way:

     last l | {append(_,[_x])=l} = _x

In the presence of different scopes, the following rules are applied:

• If a variable name of the form _x occurs in the right-hand side (and possibly in the condition) of a rule (or branch of a committed choice, see Section 7), it is considered as declared by where _x free after this rule (or branch).

• Otherwise, a variable name of the form _x is considered as introduced by let _x free in in the smallest constraint enclosing the expression. If there is no such constraint, an error is reported.

As a consequence, an expression of the form

     [\x->{append(x,_y)=[0]}, \x->{append(x,_y)=[0]}]

is interpreted as an abbreviation for

     [\x->let _y free in {append(x,_y)=[0]}, \x->let _y free in {append(x,_y)=[0]}]

i.e., the two occurrences of _y denote different objects. To avoid confusion of the exact scope of implicitly declared variables, all variables should be explicitly declared in the presence of different scopes.

2.5 Constraints and Equality

A condition of a rule is a constraint which must be solved in order to apply the rule. An elementary constraint is an equational constraint e_{1}=e_{2} between two expressions (of base type). e_{1}=e_{2} is satisfied if both sides are reducible to a same ground data term. This notion of equality, which is the only sensible notion of equality in the presence of non-terminating functions [16, 34] and also used in functional languages, is also called strict equality. As a consequence, if one side is undefined (nonterminating), then the strict equality does not hold. Operationally, an equational constraint e_{1}=e_{2} is solved by evaluating e_{1} and e_{2} to unifiable data terms. The equational constraint could also be solved in an incremental way by an interleaved lazy evaluation of the expressions and binding of variables to constructor terms (see [30] or Section D.4 in the appendix).

Equational constraints should be distinguished from standard Boolean functions (cf. Section 4.1) since constraints are checked for satisfiability. For instance, the equational constraint [x]=[0] is satisfiable if the variable x is bound to 0. However, the evaluation of [x]=[0] does not deliver a Boolean value True or False, since the latter value would require a binding of x to all values different from 0 (which could be expressed if a richer constraint system than substitutions, e.g., disequality constraints [7], is used). This is sufficient since, similarly to logic programming, constraints are only activated in conditions of equations which must be checked for satisfiability.

Note that the basic kernel of Curry only provides strict equations e_{1}=e_{2} between expressions as elementary constraints. Since it is conceptually fairly easy to add other constraint structures [32], extensions of Curry may provide richer constraint systems to support constraint logic programming applications.

Constraints can be combined into a conjunction written as {c_{1},...,c_{n}}. The conjunction is interpreted concurrently: if the combined constraint {c_{1},c_{2}} should be solved, c_{1} and c_{2} are solved concurrently. In particular, if the evaluation of c_{1} suspends, the evaluation of c_{2} can proceed which may cause the reactivation of c_{1} at some later time (due to the binding of common variables). In a sequential implementation, the evaluation of {c_{1},c_{2}} could be started by an attempt to solve c_{1}. If the evaluation of c_{1} suspends, an evaluation step is applied to c_{2}.

Syntactically, constraints are always enclosed in curly brackets. Thus, {x = f y, y = h 0} denotes the concurrent conjunction of the equational constraints x = f y and y = h 0. There is also a predefined infix operator /\ for the concurrent conjunction of two constraint which can be considered as defined by

     c1 /\ c2 = {c1, c2}

It is interesting to note that parallel functional computation models [11, 12] are covered by the use of concurrent constraints. For instance, a constraint of the form

     {x = f t1, y = g t2, z = h x y}

specifies a potentially concurrent computation of the functions f, g and h where the function h can proceed its computation only if the arguments have been bound by evaluating the expressions f t1 and g t2. Since constraints could be passed as arguments or results of functions (like any other data object or function), it is possible to specify general operators to create flexible communication architectures similarly to Goffin [12]. Thus, the same abstraction facilities could be used for sequential as well as concurrent programming. On the other hand, the clear separation between sequential and concurrent computations (e.g., a program without any occurrences of concurrent conjunctions is purely sequential) supports the use of efficient and optimal evaluation strategies for the sequential parts [4, 5], where similar techniques for the concurrent parts are not available.

2.6 Higher-order Features

Curry is a higher-order language supporting the common functional programming techniques by partial function applications and lambda abstractions. Function application is denoted by juxtaposition the function and its argument. For instance, the well-known map function is defined in Curry by

     map :: (a -> b) -> [a] -> [b]
     map f []     = []
     map f (x:xs) = f x : map f xs

However, there is an important difference w.r.t. to functional programming. Since Curry is also a logic language, it allows logical variables also for functional values, i.e., it is possible to evaluate the equation map f [1 2] = [2 3] which has, for instance, a solution {f=inc} if inc is the increment function on natural numbers. In principle, such solutions can be computed by extending (first-order) unification to higher-order unification [22, 35, 40]. Since higher-order unification is a computationally expensive operation, Curry delays the application of unknown functions until the function becomes known [2, 43]. Thus, the application operation can be considered as a function (“@” is a left-associative infix operator)

     (@) :: (a -> b) -> a -> b
     f@x = f x

which is “rigid” in its first argument (cf. Section 3).

In cases where a function is only used a single time, it is tedious to assign a name to it. For such cases, anonymous functions (λ-abstractions), denoted by

\x_{1} … x_{n}->e

are provided.

3 Operational Semantics

Curry’s operational semantics is based on the lazy evaluation of expressions combined with a possible instantiation of free variables occurring in the expression. If the expression is ground, the operational model is similar to lazy functional languages, otherwise (possibly non-deterministic) variable instantiations are performed as in logic programming. If an expression contains free variables, it may be reduced to different values by binding the free variables to different expressions. In functional programming, one is interested in the computed value, whereas logic programming emphasizes the different bindings (answers). Thus, we define for the integrated functional logic language Curry an answer expression as a pair “σ e” consisting of a substitution σ (the answer computed so far) and an expression e. An answer expression σ e is solved if e is a data term. Usually, the identity substitution in answer expressions is omitted, i.e., we write e instead of {} e if it is clear from the context.

Since more than one answer may exist for expressions containing free variables, in general, initial expressions are reduced to disjunctions of answer expressions. Thus, a disjunctive expression is a (multi-)set of answer expressions {σ_{1} e_{1}, …, σ_{n} e_{n}}. For the sake of readability, we write concrete disjunctive expressions like

{{x = 0, y = 2} 2 , {x = 1, y = 2} 3}

in the form {x=0,y=2} 2| {x=1,y=2} 3. Thus, substitutions are represented by lists of equations enclosed in curly brackets, and disjunctions are separated by vertical bars.

A single computation step performs a reduction in exactly one unsolved expression of a disjunction (e.g., in the leftmost unsolved answer expression in Prolog-like implementations). If the computation step is deterministic, the expression is reduced to a new one. If the computation step is non-deterministic, the expression is replaced by a disjunction of new expressions. The precise behavior depends on the function calls occurring in the expression. For instance, consider the following rules:

     f 0 = 2
     f 1 = 3

The result of evaluating the expression f 1 is 3, whereas the expression f x should be evaluated to the disjunctive expression

     {x=0} 2 | {x=1} 3 .

To avoid superfluous computation steps and to apply programming techniques of modern functional languages, nested expressions are evaluated lazily, i.e., the leftmost outermost function call is primarily selected in a computation step. Due to the presence of free variables in expressions, this function call may have a free variable at an argument position where a value is demanded by the left-hand sides of the function’s rules (a value is demanded by an argument position of the left-hand side of some rule, if the left-hand side has a constructor at this position, i.e., in order to apply the rule, the actual value at this position must be the constructor). In this situation there are two possibilities to proceed:

1. Delay the evaluation of this function call until the corresponding free variable is bound (this corresponds to the residuation principle which is the basis of languages like Escher [28, 29], Le Fun [2], Life [1], NUE-Prolog [37], or Oz [43]). In this case, the function is called rigid.

2. (Non-deterministically) instantiate the free variable to the different values demanded by the left-hand sides and apply reduction steps using the different rules (this corresponds to narrowing principle which is the basis of languages like ALF [18], Babel [34], K-Leaf [16], LPG [8], or SLOG [15]). In this case, the function is called flexible.

Since Curry is an attempt to provide a common platform for different declarative programming styles and the decision about the “right” strategy depends on the definition and intended meaning of the functions, Curry supports both strategies. The precise strategy is specified by evaluation annotations for each function.^{5} The general syntax for evaluation annotations can be found in Appendix C.3 and their precise operational meaning is defined in Appendix D. Usually, a function can be annotated as rigid or flexible. If an explicit annotation is not provided by the user, a default strategy is used: non-Boolean functions are always annotated with rigid arguments, and predicates (i.e., functions with the single result type Bool) with flexible arguments. Functions with a polymorphic result type (like the identity) are not considered as predicates, although they can produce Boolean values in particular cases. This default strategy can be changed by providing explicit evaluation annotations for each function or by pragmas (see Section 9).

For instance, consider the function f as defined above. If f has the evaluation annotation

     f eval flex

(i.e., f is flexible), then the expression f x is evaluated by instantiating x to 0 or 1 and applying a reduction step in both cases. This yields the disjunctive expression

     {x=0} 2 | {x=1} 3 .

However, if f has the evaluation annotation

     f eval rigid

(i.e., f is rigid), then the expression f x cannot be evaluated since the argument is a free variable. In order to proceed, we need a “generator” for values for x, which is the case in the following constraint:

     {f x = y, x = 1}

Here, the first constraint f x = y cannot be evaluated and thus suspends, but the second constraint x=1 is evaluated by binding x to 1. After this binding, the first constraint can be evaluated and the entire constraint is solved. Thus, the constraint is solved by the following steps:

     {f x = y, x = 1}
     ⇝ {x=1} {f 1 = y}
     ⇝ {x=1} {3 = y}
     ⇝ {x=1,y=3}

(The empty constraint is omitted in the final answer.)

4 Types

4.1 Built-in Types

The following types are predefined in Curry:

5Evaluation annotations are similar to coroutining declarations [36] in Prolog where the programmer specifies conditions under which a literal is ready for a resolution step. Moreover, they describe the strategy to evaluate different and nested arguments.

Boolean values: They are predefined by the datatype declaration

     data Bool = True | False

The (sequential) conjunction is predefined as the left-associative infix operator &&:

     (&&) :: Bool -> Bool -> Bool
     True  && x = x
     False && x = False

Similarly, negation is predefined as:

     not :: Bool -> Bool
     not True  = False
     not False = True

Boolean values are mainly used in conditionals, i.e., the conditional function if_then_else is predefined as

     if_then_else :: Bool -> a -> a -> a
     if True  then x else y = x
     if False then x else y = y

where if b then x else y is syntactic sugar for the application if_then_else b x y. A function with result type Bool is also called a predicate. There are a number of builtin predicates for comparing objects, like the predicate “<” to compare numbers (e.g., 1<2 evaluates to True and 4<3 evaluates to False). There is also a standard predicate “==” to test the convertibility of expressions to identical data terms (“strict equality”, cf. Section 2.5): e_{1}==e_{2} reduces to True if e_{1} and e_{2} are reducible to identical ground data terms, and it reduces to False if e_{1} and e_{2} are reducible to different ground data terms. The evaluation of e_{1}==e_{2} suspends if one of the arguments is a free variable (i.e., == is a “rigid” function, cf. Section 3). If neither e_{1} nor e_{2} is a free variable, e_{1}==e_{2} is reduced according to the following rules:

C == C = True % for all 0-ary constructors C C x_{1} … x_{n} == C y_{1} … y_{n} = x_{1}==y_{1} &&...&& x_{n}==y_{n} % for all n-ary constructors C C x_{1} … x_{n} == D y_{1} … y_{m} = False % for all different constructors C and D

This implements a test for strict equality (cf. Section 2.5). For instance, the test “[0]==[0]” reduces to True, whereas the test “1==0” reduces to False. An equality test with a free variable in one side is delayed in order to avoid an infinite set of solutions for insufficiently instantiated tests like x==y. Usually, strict equality is only defined on data terms, i.e., == is not really polymorphic but an overloaded function symbol. This could be more precisely expressed using type classes which will be considered in a future version. Note that e_{1}==e_{2} only tests the identity of e_{1} and e_{2} but never binds one side to the other if it is a free variable. This is in contrast to solving the equational constraint e_{1}=e_{2} which is checked for satisfiability and propagates new variable bindings in order to solve this constraint. Thus, in terms of concurrent constraint programming languages [41], == and = correspond to ask and tell equality constraints, respectively.

Constraints: The type Constraint is the type of a constraint which is used in conditions of defining rules. Constraints are different from Boolean values: a Boolean expression reduces to True or False whereas a constraint is checked for satisfiability. A constraint is applied (i.e., solved) in a condition of a conditional equation. The equational constraint e_{1}=e_{2} is an elementary constraint which is solvable if the expressions e_{1} and e_{2} are evaluable to unifiable data terms. Constraints can be combined into a conjunction of the form {c_{1},c_{2},...,c_{n}}. In case of n = 0, “{}” denotes an empty, i.e., always solvable constraint. Otherwise, all constraints in the conjunction are evaluated concurrently. Constraints can be passed as parameters or results of functions like any other data object. For instance, the following function takes a list of constraints as input and produces a single constraint, the conjunction of all constraints of the input list:

     conj :: [Constraint] -> Constraint
     conj []     = {}
     conj (c:cs) = {c, conj cs}

The trivial constraint {} is usually not shown in answers to a constraint expression. For instance, the constraint {x*x=y, x=2} is evaluated to the answer

     {x=2, y=4}

Functions: The type t1 -> t2 is the type of a function which produces a value of type t2 for each argument of type t1. A function f is applied to an argument x by writing “f x”. The type expression

t_{1} -> t_{2} -> ⋯ -> t_{n+1}

is an abbreviation for the type

t_{1} -> (t_{2} -> (⋯ -> t_{n+1}))

and denotes the type of a (currified) n-ary function, i.e., -> associates to the right. Similarly, the expression

f e_{1} e_{2} … e_{n}

is an abbreviation for the expression

(...((f e_{1}) e_{2}) … e_{n})

and denotes the application of a function f to n arguments, i.e., the application associates to the left.

Integers: The common integer values, like “42” or “-15”, are considered as constructors (constants) of type Int. The usual operators on integers, like + or *, are predefined functions with “rigid” arguments, i.e., are evaluated only if both arguments are integer values, otherwise such function calls are delayed. Thus, these functions can be used as “passive constraints” which become active after binding their arguments. For instance, if the predicate digit is defined by the equations

     digit 0 = True
     ...
     digit 9 = True

then the constraint {x*x=y, x+x=y, digit x = True} is solved by delaying the two equations which will be activated after binding the variable x to a digit by the predicate call digit x. Thus, the corresponding computed solution is

     {x=0,y=0} | {x=2,y=4}

Floating point numbers: Similarly to integers, values like “3.14159” or “5.0e-4” are considered as constructors of type Float. Since overloading is not included in the kernel version of Curry, the names of arithmetic functions on floats are different from the corresponding functions on integers.

Lists: The type [t] denotes all lists whose elements are values of type t. The type of lists can be considered as predefined by the declaration

     data [a] = [] | a : [a]

where [] denotes the empty list and x:xs is the non-empty list consisting of the first element x and the remaining list xs. Since it is common to denote lists with square brackets, the following convenient notation is supported:

     [e_{1},e_{2},...,e_{n}]

denotes the list e_{1}:e_{2}:⋯:e_{n}:[] (which is equivalent to e_{1}:(e_{2}:(⋯:(e_{n}:[])...)) since “:” is a right-associative infix operator). Note that there is an overloading in the notation [t]: if t is a type, [t] denotes the type of lists containing elements of type t, where [t] denotes a single element list (with element t) if t is an expression. Since there is a strong distinction between occurrences of types and expressions, this overloading can always be resolved. For instance, the following predefined functions define the concatenation of two lists and the application of a function to all elements in a list:

     (++) :: [a] -> [a] -> [a]
     []     ++ ys = ys
     (x:xs) ++ ys = x : xs ++ ys
     map :: (a -> b)  -> [a] -> [b]
     map f []     = []
     map f (x:xs) = f x : map f xs

Characters: Values like 'a' or '0' denote constants of type Char. There are two conversion functions between characters and their corresponding ASCII values:

     ord :: Char -> Int
     chr :: Int -> Char

Strings: The type String is an abbreviation for [Char], i.e., strings are considered as lists of characters. String constants are enclosed in double quotes. Thus, the string constant "Hello" is identical to the character list ['H','e','l','l','o']. A term can be converted into a string by the function

          show :: a -> String

For instance, the result of show(42) is the character list ['4','2'].

Tuples: If t_{1}, t_{2}, …, t_{n} are types and n ≥ 2, then (t_{1},t_{2},...,t_{n}) denotes the type of all n-tuples. The elements of type (t_{1},t_{2},...,t_{n}) are (x_{1},x_{2},...,x_{n}) where x_{i} is an element of type t_{i} (i = 1, …, n). Thus, for each n, the tuple-building operation (…) can be considered as an n-ary constructor introduced by the pseudo-declaration

data (a_{1},a_{2}, …,a_{n}) = (·) a_{1} a_{2}...a_{n}

where (x_{1},x_{2},...,x_{n}) is equivalent to the constructor application (·) x_{1} x_{2}...x_{n}. The unit type () has only a single element () and can be considered as defined by

          data () = ()

Thus, the unit type can also be interpreted as the type of 0-tuples.

4.2 Type System

Curry is a strongly typed language with a Hindley/Milner-like polymorphic type system [13].^{6} Each variable, constructor and operation has a unique type, where only the types of constructors have to be declared by datatype declarations (see Section 2.1). The types of functions can be declared (see Section 2.2) but can also be omitted. In the latter case they will be reconstructed by a type inference mechanism.

Note that Curry is an explicitly typed language, i.e., each function has a type. The type can only be omitted if the type inferencer is able to reconstruct it and to insert the missing type declaration. In particular, the type inferencer can reconstruct only those types which are visible in the module (cf. Section 5).

To do: Define typing rules.

5 Modules

A module defines a collection of datatypes, constructors and functions which we call entities in the following. A module exports some of its entities which can be imported and used by other modules. An entity which is not exported is not accessible from other modules.

A Curry program is a collection of modules. There is one main module which is loaded into a Curry system. The modules imported by the main module are implicitly loaded but not visible to the user. After loading the main module, the user can evaluate expressions which contain entities exported by the main module.

6The extension of the type system to Haskell’s type classes is not included in the kernel language but may be considered in a future version.

There is one distinguished module, named prelude, which is implicitly imported into all programs (see also Appendix B). Thus, the entities defined in the prelude (basic functions for arithmetic, list processing etc.) can be always used.

A module always starts with the head which contains at least the name of the module followed by the keyword where, like

     module stack where ...

If a program does not contain a module head, the standard module head “module main where” is implicitly inserted. Module names can be given a hierarchical structure by inserting dots which is useful if larger applications should be structured into different subprojects, e.g.,

     company.project1.subproject2.mod4

is a valid module name. The dots may reflect the hierarchical file structure where modules are stored. For instance, the module compiler.symboltable could be stored in the file

symboltable.cur in the directory compiler.

Without any further restrictions in the module head, all entities which are directly accessible (see below) in the module (roughly speaking, all entities defined or imported in the module) are exported. In order to restrict the set of exported entities of a module, an export list can be added to the module head. For instance, a module with the head

     module stack(stackType, push, pop, newStack) where ...

exports the entities stackType, push, pop, and newStack. An export list can contain the following entries:

1. Names of datatypes: This exports only the datatype, whose name must be directly accessible in this module, but not the constructors of the datatype. The export of a datatype without its constructors allows the definition of abstract datatypes.

2. Datatypes with constructors: If the export list contains the entry t(c_{1},...,c_{n}), then t must be a datatype directly accessible in the module and c_{1},…,c_{n} are directly accessible constructors of this datatype. In this case, the datatype t and the constructors c_{1},…,c_{n} are exported by this module.

3. Datatypes with all constructors: If the export list contains the entry t(..), then t must be a datatype whose name is directly accessible in the module. In this case, the datatype t and all constructors of this datatype, which must be also directly accessible in this module, are exported.

4. Names of functions: This exports the corresponding functions whose names must be directly accessible in this module. The types occurring in the argument and result type of this function are implicitly exported, otherwise the function may not be applicable outside this module.

5. Modules: The set of all directly accessible entities imported from a module m into the current module (see below) can be exported by a single entry “module m” in the export list. For instance, if the head of the module stack is defined as above, the module head

          module queue(module stack, enqueue, dequeue) where ...

specifies that the module queue exports the entities stackType, push, pop, newStack,

     enqueue, and dequeue.

If the exported entities from imported modules should be further restricted, one can also add an export list to the exported module. This list can contain names of datatypes and functions imported from this module. If a datatype which is imported from another module is exported, the datatype is exported in the same way (i.e., with or without constructors) how it is imported into the current module. Thus, a further specification for the exported constructors is not necessary. For instance, the module head

          module queue(module stack(stackType,newStack), enqueue, dequeue) ...

specifies that the module queue exports the entities stackType and newStack, which are imported from stack, and enqueue and dequeue, which are defined in queue.

All entities defined by top-level declarations in a module are directly accessible in this module. Additionally, the entities exported by another module can be also made directly accessible in the module by an import declaration. An import declaration consists of the name of the imported module and (optionally) a list of entities imported from that module. If the list of imported entities is omitted, all entities exported by that module are imported. For instance, the import declaration

     import stack

imports all entities exported by the module stack, whereas the declaration

     import family(father, grandfather)

imports only the entities father and grandfather from the module family, provided that they are exported by family.

The names of all imported entities are directly accessible in the current module, i.e., they are equivalent to top-level declarations, provided that their names are not in conflict with other names. For instance, if a function f is imported from module m but the current module contains a top-level declaration for f (which is thus directly accessible in the current module), the imported function is not directly accessible. Similarly, if two identical names are imported from different modules, none of these entities is directly accessible. It is possible to access imported but not directly accessible names by prefixing them with the module identifier. For instance, consider the module m1 defined by

     module m1 where
     f :: Int -> Int
     ...

and the module m2 defined by

     module m2 where
     f :: Int -> Int
     ...

together with the main module

module main where
import m1
import m2
...

Then the names of the imported functions f are not directly accessible in the main module but one can refer by the qualified identifiers m1.f or m2.f to the corresponding imported entities. Note that export declarations only allow unqualified names to be exported (which is the reason for the direct accessibility condition for the exports). This prevents hierarchical qualifications like mod1.mod2.f and supports the view to consider a module as a single collection of related entities.

Another method to resolve name conflicts between imported entities is the renaming of imported entities. For instance, the name conflict between m1.f and m2.f can be resolved by the following imports:

module main where
import m1
import m2 renaming f to m2_f
...

Thus, the entity f exported by module m2 is imported with the name m2_f. In the subsequent body of this module, the (directly accessible) name f refers to the entity exported by module m1 and the (directly accessible) name m2_f refers to the entity f exported by module m2. Only imported entities can be renamed, i.e., the import declaration

import m(f) renaming g to mg

will always cause an error.

Although each name refers to exactly one entity, it is possible that the same entity is referred by different names. For instance, consider the module m defined by

module m(f) where
f :: Int -> Int
...

and the module use_m defined by

module use_m(f) where
import m

together with the main module

module main where
import m renaming f to mf
import use_m
...

Then the names mf as well as f refers in the main module to the same function defined in module

m.

The import dependencies between modules must be non-circular, i.e., it is not allowed that module m_{1} imports module m_{2} and module m_{2} also imports (directly or indirectly) module m_{1}.

6 Input/Output

Curry provides a declarative model of I/O by considering I/O operations as transformations on the outside world. In order to avoid dealing with different versions of the outside world, it must be ensured that at each point of a computation only one version of the world is accessible. This is guaranteed by using the monadic I/O approach [39] of Haskell and by requiring that I/O operations are not allowed in program parts where non-deterministic search is possible.

In the monadic I/O approach, the outside “world” is not directly accessible but only through actions which change the world. Thus, the world is encapsulated in an abstract datatype which provides actions to change the world. The type of such actions is IO t which is an abbreviation for

     World -> (t,World)

where World denotes the type of all states of the outside world. If an action of type IO t is applied to a particular world, it yields a value of type t and a new (changed) world. For instance, getChar is an action which reads a character from the standard input when it is executed, i.e., applied to a world. Therefore, getChar has the type IO Char. The important point is that values of type World are not accessible for the programmer — she/he can only create and compose actions on the world. Thus, a program intended to perform I/O operations has a sequence of actions as the result. These actions are computed and executed when the program is connected to the world by executing it. For instance,

     getChar :: IO Char
     getLine :: IO String

are actions which read the next character or the next line from the standard input. The functions

     putChar  :: Char -> IO ()
     putStr   :: String -> IO ()
     putStrLn :: String -> IO ()

take a character (string) and produces an action which, when applied to a world, puts this character (string) to the standard output (and a line-feed in case of putStrLn.

Since an interactive program consists of a sequence of I/O operations, where the order in the sequence is important, there are two operations to compose actions in a particular order. The function

     (>>) :: IO a -> IO b -> IO b

takes two actions as input and yields an action as output. The output action consists of performing the first action followed be the second action, where the produced value of the first action is ignored. If the value of the first action should be taken into account before performing the second action, the actions can be composed by the function

     (>>=) :: IO a -> (a -> IO b) -> IO b

where the second argument is a function taking the value produced by the first action as input and performs another action. For instance, the action

     getLine >>= putStrLn

is of type IO () and copies, when executed, a line from standard input to standard output. The return function

     return :: a -> IO a

is sometimes useful to terminate a sequence of actions and return a result of an I/O operation. Thus, return v is an action which does not change the world and returns the value v.

To execute an action, it must be the main expression in a program, i.e., interactive programs have type IO (). Since the world cannot be copied (note that the world contains at least the complete file system), non-determinism in relation with I/O operations must be avoided. Thus, the applied action must always be known, i.e., >> and >>= are rigid in their arguments. Moreover, it is a runtime error if a disjunctive expression (cf. Section 3) σ_{1} e_{1} |⋯| σ_{n} e_{n}, where the e_{i}’s are of type IO (), occurs as the top-level expression of a program, since it is unclear in this case which of the disjunctive actions should be applied to the current world. Thus, all possible search must be encapsulated between I/O operations (see Section 7).

Using the evaluation annotations, a compiler is able to detect functions where search is definitely avoided (e.g., if all evaluated positions are declared as rigid). Thus, the compiler may warn the user about non-deterministic computations which may occur in I/O actions so that the programmer can encapsulate them.

7 Encapsulated Search

Global search, possibly implemented by backtracking, must be avoided in some situations (usercontrol of efficiency, concurrent computations, non-backtrackable I/O). Hence it is sometimes necessary to encapsulate search, i.e., non-deterministic computations in parts of larger programs. Non-deterministic computations might occur in Curry whenever a function must be evaluated with a free variable at a flexible argument position. In this case, the computation must follow different branches with different bindings applied to the current expression which has the effect that the entire expression is split into (at least) two independent disjunctions. To give the programmer control on the actions taken in this situation, Curry provides a primitive search operator which is the basis to implement sophisticated search strategies. This section sketches the idea of encapsulating search in Curry and describes some predefined search strategies.

7.1 Search Goals and Search Operators

Since search is used to find solutions to some constraint, search is always initiated by a constraint containing a search variable for which a solution should be computed.^{7} Since the search variable may be bound to different solutions in different disjunctive branches, it must be abstracted. Therefore, a search goal has the type a->Constraint where a is the type of the values which we are searching for. In particular, if c is a constraint containing a variable x and we are interested in solutions for x, i.e., values for x such that c is satisfied, then the corresponding search goal has the form \x->c. However, any other expression of the same type can also be used as a search goal.

7The generalization to more than one search variable is straightforward by the use of tuples.

To control the search performed to find solutions to search goals, Curry has a predefined operator

try :: (a->Constraint) -> [a->Constraint]

which takes a search goal and produces a list of search goals. The search operator try attempts to evaluate the search goal until the computation finishes or performs a non-deterministic splitting. In the latter case, the computation is stopped and the different search goals caused by this splitting are returned as the result list. Thus, an expression of the form try \x->c can have three possible results:

1. An empty list. This indicates that the search goal \x->c has no solution. For instance, the expression

     try \x -> {1=2}

reduces to [].

2. A list containing a single element. In this case, the search goal \x->c has a single solution represented by the element of this list. For instance, the expression

     try \x->{[x]=[0]}

reduces to [\x->{x=0}]. Note that a solution, i.e., a binding for the search variable like the substitution {x ↦ 0}, can always be presented by an equational constraint like {x=0}.

3. A list containing more than one element. In this case, the evaluation of the search goal \x->c requires a non-deterministic computation step. The different alternatives immediately after this non-deterministic step are represented as elements of this list. For instance, if the function f is defined by

     f eval flex
     f a = c
     f b = d

then the expression

     try \x->{f x = d}

reduces to the list [\x->{x=a, f a = d}, \x->{x=b, f b = d}]. This example also shows why the search variable must be abstracted: the alternative bindings cannot be actually performed (since a free variable is only bound to at most one value in each computation thread) but are represented as equational constraints in the search goal.

Note that the search goals of the list in the last example are not further evaluated. This provides the possibility to determine the behavior for non-deterministic computations. For instance, the following function defines a depth-first search operator which collects all solutions of a search goal in a list:

all :: (a->Constraint) -> [a->Constraint]
all g = collect (try g)
      where collect []         = []

                 collect [g]        = g
                 collect (g1:g2:gs) = concat (map all (g1:g2:gs))

(concat concatenates a list of lists to a single list). For instance, if append is the list concatenation (and defined as flexible), then the expression

     all \l->{append l [1] = [0,1]}

reduces to [\l->{l=[0]}].

The value computed for the search variable in a search goal can be easily accessed by applying it to a free variable. For instance, the evaluation of the applicative expression

     {all \l->{append l [1] = [0,1]} = [g], g x}

binds the variable g to the search goal [\l->{l=[0]}] and the variable x to the value [0] (due to solving the constraint {x=[0]}). Based on this idea, there is a predefined function

     findall :: (a->Constraint) -> [a]

which takes a search goal and collects all solutions (computed by a depth-first search like all) for the search variable into a list.

Due to the laziness of the language, search goals with infinitely many solutions cause no problems if one is interested only in finitely many solutions. For instance, a function which computes only the first solution w.r.t. a depth-first search strategy can be defined by

     first g = head (findall g)

Note that first is a partial function, i.e., it is undefined if g has no solution.

7.2 Local Variables

Some care is necessary if free variables occur in the search goal, like in the goal

     \l2->{append l1 l2 = [0,1]}

Here, only the variable l2 is abstracted in the search goal but l1 is free. Since non-deterministic bindings cannot be performed during encapsulated search, free variables are never bound inside encapsulated search. Thus, if it is necessary to bind a free variable in order to proceed an encapsulated search operation, the computation suspends. For instance, the expression

     first \l2->{append l1 l2 = [0,1]}

cannot be evaluated and will be suspended until the variable l1 is bound by another part of the computation. Thus, the constraint

     {s = first \l2->{append l1 l2 = [0,1]}, l1 = [0]}

can be evaluated since the free variable l1 in the search goal is bound to [0], i.e., this constraint reduces to the answer

     {l1=[0], s=[1]}

In some cases it is reasonable to have unbound variables in search goals, but these variables should be treated as local, i.e., they might have different bindings in different branches of the search. For instance, if we want to compute the last element of the list [3,4,5] based on append, we could try to solve the search goal

     \e -> {append l [e] = [3,4,5]}

However, the evaluation of this goal suspends due to the necessary binding of the free variable l. This can be avoided by declaring the variable l as local to the constraint by the use of let (see Section 2.4), like in the following expression:

     first \e -> let l free in {append l [e] = [3,4,5]}

Due to the local declaration of the variable l (which corresponds logically to an existential quantification), the variable l is only visible inside the constraint and, therefore, it can be bound to different values in different branches. Hence this expression evaluates to the result 5.

In order to ensure that an encapsulated search will not be suspended due to necessary bindings of free variables, the search goal should be a closed expression when a search operator is applied to it, i.e., the search variable is bound by the lambda abstraction and all other free variables are existentially quantified by local declarations.

7.3 Predefined Search Operators

There are a number of search operators which are predefined in the prelude. All these operators are based on the primitive try as described above. It is also possible to define other search strategies in a similar way. Thus, the try operator is a a powerful primitive to define appropriate search strategies. In the following, we list the predefined search operators.

all ::  (a->Constraint) -> [a->Constraint]

Compute all solutions for a search goal via a depth-first search strategy. If there is no solution and the search space is finite, the result is the empty list, otherwise the list contains solved search goals (i.e., without defined operations).

once ::  (a->Constraint) -> (a->Constraint)

Compute the first solution for a search goal via a depth-first search strategy. Note that once is partially defined, i.e., if there is no solution and the search space is finite, the result is undefined.

findall ::  (a->Constraint) -> [a]

Compute all solutions for a search goal via a depth-first search strategy and unpack the solution’s values for the search variable into a list.

best ::  (a->Constraint) -> (a->a->Bool) -> [a->Constraint]

Compute the best solution via a depth-first search strategy, according to a specified relation (the second argument) that can always take a decision which of two solutions is better (the relation should deliver True if the first argument is a better solution than the second argument). This operator is only used for a test, i.e., it should be a rigid function. As a trivial example, consider the relation shorter defined by

          shorter l1 l2 = length L1 <= length l2

Then the expression

     best (\x -> let y free in {append x y = [1,2,3]}) shorter

computes the shortest list which can be obtained by splitting the list [1,2,3] into this list and some other list, i.e., it reduces to [\x->{x=[]}]. Similarly, the expression

     best (\x -> let y free in {append x y = [1,2,3]})
          (\l1 l2 -> length l1 > length l2)
reduces to [\x->x=[1,2,3]].
one ::  (a->Constraint) -> [a->Constraint]

Compute one solution via a fair strategy. If there is no solution and the search space is finite, the result is the empty list, otherwise the list contains one element (the first solution represented as a search goal).

condSearch ::  (a->Constraint) -> (a->Bool) -> [a->Constraint]

Compute the first solution (via a fair strategy) that meets a specified condition. The condition (second argument) must be a unary Boolean function.

browse ::  (a->Constraint) -> IO ()

Show the solution of a solved constraint on the standard output, i.e., a call browse g, where g is a solved search goal, is evaluated to an I/O action which prints the solution. If g is not an abstraction of a solved constraint, a call browse g produces a runtime error.

browseList ::  [a->Constraint] -> IO ()

Similar to browse but shows a list of solutions on the standard output. The browse operators are useful for testing search strategies. For instance, the evaluation of the expression

     browseList (all \x -> let y free in {append x y = [0,1,2]})

produces the following result on the standard output:

     []
     [0]
     [0,1]
     [0,1,2]

Due to the laziness of the evaluation strategy, one can also browse the solutions of a goal with infinitely many solutions which are printed on the standard output until the process is stopped.

7.4 Choice

In order to provide a “don’t care” selection of an element out of different alternatives, which is necessary in concurrent computation structures to support many-to-one communication, Curry provides a primitive choice operation of the form

choice {c_{1}} -> e_{1} where localdecls_{1} {c_{2}} -> e_{2} where localdecls_{2}

⋮
{c_{n}} -> e_{n} where localdecls_{n}

where e_{1}, …, e_{n} are expressions of the same type and c_{1}, …, c_{n} are constraints. The optional where-clause in each branch can be omitted. These clauses are useful to define free variables which are only visible in the constraint c_{k} and the expression e_{k} of the corresponding branch (cf. Section 2.4).

Such a choice expression reduces to some e_{i} when the corresponding constraint is entailed, i.e., if, for some i ∈ {1, …, n}, c_{i} is evaluable to ⋯| σ |⋯ where σ does only bind variables introduced in the choice branch (including the where-clause), then the entire choice expression reduces to the single expression σ(e_{i}).^{8} This can be implemented by evaluating each c_{i} (with a fair strategy) as usual but with the restriction that only local variables can be bound, similarly to the search operators (see above).

Note that functions containing choice expressions may be non-deterministic in contrast to other user-defined functions. Although one could argue that this destroys the declarative reading of programs, it is possible to provide a declarative semantics even for non-deterministic functions w.r.t. strict equality [17]. However, the completeness result for Curry’s operational semantics [21] does not hold in the presence of the choice construct. Nevertheless, the choice is useful in a number of applications, as shown in the following.

The non-deterministic function merge, which merges two lists, can be defined as follows:

     merge :: [a] -> [a] -> [a]
     merge l1 l2 = choice {l1=[]} -> l2
                          {l2=[]} -> l1
                          {l1=e:r} -> e:merge r l2  where e,r free
                          {l2=e:r} -> e:merge l1 r  where e,r free

Since the constraints in choice branches are only checked for entailment, the entire choice can be reduced only if one of the input lists is known to be empty or non-empty. Thus, merge can also merge partially unknown lists which are incrementally instantiated during computation.

8 Interface to External Functions and Constraint Solvers

Since Curry has only a small number of builtins, it provides a simple interface to connect external functions (functions programmed in another language) and external constraint solvers. External functions must be free of side-effects in order to be compatible with Curry’s computation model. An external constraint solver consists of a constraint store which can be accessed and manipulated via a few primitive operations.

8.1 External Functions

External functions are considered as an implementation of a potentially infinite set of equations (describing the graph of the functions). In particular, they have no side effects, i.e., identical function calls at different points of time yield identical results. Since the implementation of an external function is unknown, a call to an external function is suspended until all arguments are fully known, i.e., until they are evaluated to ground data terms. This view is compatible with the residuation principle covered by Curry’s computation model and very similar to the connection of external functions to logic programs [9, 10].

8The choice corresponds to the committed choice (with deep guards) of concurrent logic languages.

An external function is declared by a type declaration followed by external(FName,OF,Lang) where FName is the name of the external function where its code is contained in the object file OF. Lang is the implementation language of the external function. For instance, if the addition and multiplication on integers are defined as C functions named add and mult where the compiled code is contained in the file “arith.o”, we can connect these functions to a Curry program by providing the declarations

     add  :: Int -> Int -> Int  external("add","arith.o",C)
     mult :: Int -> Int -> Int  external("mult","arith.o",C)

Implementations of Curry might have restrictions on the interface. A reasonable requirement is that the implementation language is constrained to C and the argument and result types are only

simple types like Bool, Int, Float, Char, or String.

8.2 External Constraint Solvers

A constraint solver can be viewed as an abstract datatype consisting of a constraint store together with a few operations to check the entailment of a constraint or to add a new constraint. In order to connect a constraint solver to Curry, like a solver for arithmetic or Boolean constraints, the external solver must provide the following operations (cs denotes the type of the constraint store and c the type of constraints):

new :  → cs  (create and initialize a new constraint store)
ask : cs × c → {T rue, F alse, Unknown} (check entailment of a constraint)
tell : cs × c → cs  (add a new constraint)
clone : cs  → cs × cs  (copy the constraint store)

Using these operations, it is relatively easy to extend Curry’s computation model to include constraints by adding the constraint store as a new component to the substitution part in answer expressions (cf. Section 3).

To do: Describe the connection in more detail.

9 Pragmas

Curry is a multi-paradigm language providing different programming styles, like functional programming, logic programming, and functional logic programming based on narrowing or residuation. As described in Section 3, the difference between narrowing (non-deterministic evaluation of functions) and residuation (delayed evaluation of functions) is specified by evaluation annotations for each function. Since the specification of the evaluation annotations is tedious, they are automatically generated using a default strategy (pattern matching from left to right, rigid branches for non-Boolean functions, flexible branches for predicates, see Appendix D.6). This default strategy can be overridden by providing explicit evaluation annotations for each function or by a pragma which changes the default strategy for the entire module where they occur (but not for the imported modules):

     pragma p

If p = flex, then all functions are flexible if not specified otherwise. If p = rigid, then all functions (including the Booleans ones) are rigid if not specified otherwise. If p = optmatch, then the compiler tries to find pattern matching strategies with a better termination behavior than the strict left-to-right pattern matching (i.e., the compiler generates evaluation annotations without or annotations for inductively sequential programs, see [3, 21] and Appendix D.6 for more details).

10 Interactive Programming Environment

In order to support different implementations with a comparable user interface, the following commands should be supported by each interactive programming environment for Curry:

:l file Load the program stored in file.

expr Evaluate the expression expr.

:d expr Debug the evaluation of the expression expr, i.e., show the single computation steps and ask the user what to do after each single step (like proceed, abort, etc.).

:t f Show the type of function f.

:e f Show the evaluation annotation of function f.

:q Exit the system.

To do: Describe the debugger in more detail.

A Example Programs

This section contains a few example programs together with some initial expressions and their computed results.

A.1 Operations on Lists

Here are simple operations on lists. Note that append has a “flexible” evaluation annotation so that it can also be applied to solve equations containing append, i.e., append can be used to split lists. We exploit this property to define the list membership in a very simple way.

% Concatenation of two lists:
append :: [t] -> [t] -> [t]
append eval flex
append []     ys = ys
append (x:xs) ys = x:append xs ys
% Naive reverse of all list elements:
rev :: [t] -> [t]
rev []     = []
rev (x:xs) = append (rev xs) [x]
% List membership using concatenation:
member :: t -> [t] -> Bool
member e xs  | {append _(e:_) = xs} = True

Expressions and their evaluated results:

append [0,1] [2,3] ⇝ [0,1,2,3]
{append L M = [0,1]}
   ⇝ {L=[],M=[0,1]} | {L=[0],M=[1]} | {L=[0,1],M=[]}
rev [0,1,2,3] ⇝ [3,2,1,0]
member X [0,1,2] && member X [1,2,3] ⇝ {X=1} True | {X=2} True

A.2 Higher-Order Functions

Here are some “traditional” higher-order functions to show that the familiar functional programming techniques can be applied in Curry.

% Map a function on a list (predefined):
map :: (t1->t2) -> [t1] -> [t2]
map f []     = []
map f (x:xs) = f x:map f xs
% Fold a list (predefined):
foldr :: (t1->t2->t2) -> t2 -> [t1] -> t2
foldr f a []     = a
foldr f a (x:xs) = f x (foldr f a xs)
% Filter elements in a list (predefined):
filter :: (t -> Bool) -> [t] -> [t]
filter p []     = []
filter p (x:xs) = if p x then x:filter p xs
                         else filter p xs
% Quicksort function:
quicksort :: [Int] -> [Int]
quicksort []      = []
quicksort (x:xs)  = quicksort (filter (<= x) xs)
                    ++ [x]
                    ++ quicksort (filter (> x) xs)

A.3 Relational Programming

Here is a traditional example from logic programming: a simple deductive database with family relationships.

% Declaration of an enumeration type for persons:
% (as an alternative, one could consider persons as strings)
data Person = christine | maria | monica | alice | susan |
              antony | bill | john | frank | peter | andrew
% Two basic relationships:
married :: Person -> Person -> Bool
married christine antony = True
married maria     bill   = True
married monica    john   = True
married alice     frank  = True
mother :: Person -> Person -> Bool
mother christine john   = True
mother christine alice  = True
mother maria     frank  = True
mother monica    susan  = True
mother monica    peter  = True
mother alice     andrew = True
% and here are the deduced relationships:
father :: Person -> Person -> Bool
father f c  | married m f && mother m c  = True
grandfather :: Person -> Person -> Bool
grandfather g c  | father g _f && father _f c  = True
grandfather g c  | father g _m && mother _m c  = True

Expressions and their evaluated results:

father john Child ⇝ {Child=susan} True | {Child=peter} True
grandfather G C ⇝
{G=antony,C=susan} True | {G=antony,C=peter} True |
{G=bill,C=andrew} True | {G=antony,C=andrew} True

A.4 Constraint Solving and Concurrent Programming

In this example we demonstrate how Curry’s concurrent features can be used to solve constraint problems with finite domains more efficiently than a simple generate-and-test solver. We want to solve the classical map coloring problem. Consider the following simple map:

Country 1

\frac{Country 2}{Country 3}

Country 4

The problem is to assign to each of the four countries a color (red, green, yellow, or blue) such that countries with a common border have different colors.

To solve this problem, we have to specify that some countries have different colors. For this purpose, we define the following constraint which checks to elements for incompatibility:

     diff :: a -> a -> Constraint
     diff x y = {(x==y)=False}

For instance, diff t_{1} t_{2} is satisfied if t_{1} and t_{2} are different constants. If one of the arguments is a variable, the evaluation of the function is delayed by definition of ==.

Now there is a straightforward solution of the map coloring problem. We define a predicate coloring specifying the valid colors for each country and a predicate correct specifying which countries must have different colors:

     data Color = Red | Green | Yellow | Blue
     color :: Color -> Bool
     color Red    = True
     color Yellow = True
     color Green  = True
     color Blue   = True
     coloring :: Color -> Color -> Color -> Color -> Bool
     coloring l1 l2 l3 l4 = color l1 && color l2 && color l3 && color l4
     correct :: Color -> Color -> Color -> Color -> Constraint
     correct l1 l2 l3 l4 = {diff l1 l2, diff l1 l3, diff l2 l3,
                            diff l2 l4, diff l3 l4}

In classical logic programming, we can compute the solutions to the map coloring problem by enumerating all potential solutions followed by a check whether a potential solution is a correct one (“generate and test”). This can be expressed by solving the following goal:

     {coloring l1 l2 l3 l4 = True, correct l1 l2 l3 l4}

However, a much faster solution can be obtained by reversing the order of the test and generate predicates:

     {correct l1 l2 l3 l4, coloring l1 l2 l3 l4 = True}

The latter constraint is evaluated in a concurrent way. In the first steps, the subexpression correct l1 l2 l3 l4 is reduced to the constraint

     {diff l1 l2, diff l1 l3, diff l2 l3, diff l2 l4, diff l3 l4}

which is then reduced to

     {(l1==l2)=False, (l1==l3)=False, (l2==l3)=False, (l2==l4)=False, (l3==l4)=False}

This constraint cannot be further evaluated since the arguments to == are free variables. Therefore, it is delayed and the final equational constraint coloring l1 l2 l3 l4 = True is evaluated which binds the variables to the potential colors. Since the variable binding is performed by consecutive computation steps, the equalities are evaluated as soon as their arguments are bound. For instance, if the variables l1 and l2 are bound to the color red, the first constraint (l1==l2)=False cannot be solved (due to the unsolvability of the equational constraint True=False) which causes the failure of the entire goal. As a consequence, not all potential colorings are computed (as in the generateand-test approach) but only those colorings for which the constraints correct l1 l2 l3 l4 is satisfiable. Therefore, the (dis)equality goals act as “passive constraints” aiming to reduce the search space.

A.5 Concurrent Object-Oriented Programming

The following example shows a simple method to program in a concurrent object-oriented style in Curry. For this purpose, an object is a process waiting for incoming messages. The local state is a parameter of this process. Thus, a process is a function of type

[Message] -> State -> Constraint

In the subsequent example, we implement a bank account as an object waiting for messages of the form Deposit i, Withdraw i, or Balance i. Thus, the bank account can be defined as follows:

data Message = Deposit Int | Withdraw Int | Balance Int
account :: [Message] -> Int -> Constraint
account [] _= {}
account (Deposit  a : ms) n = {account ms (n+a)}
account (Withdraw a : ms) n = {account ms (n-a)}
account (Balance  b : ms) n = {b=n, account ms n}
-- Install an initial account with message stream s:
make_account s = account s 0

A new account object is created by the constraint make_account S where S is a free variable. When S is instantiated with messages, the account process starts processing these messages. The following concurrent conjunction of constraints creates an account and sends messages:

{make_account S, S=[Deposit 200, Deposit 50, Balance B]}

After this goal is solved, the free variable B has been bound to 250 representing the balance after the two deposits.

To show a client-server interaction, we define a client of a bank account who is finished if his account is 50, buys things for 30 if his account is greater than 50, and works for an income of 70 if his account is less than 50. In order to get the client program independent of the account processing, the client sends messages to his account. Therefore, the client is implemented as follows:

-- Send a message to an object identified by its message stream obj:
send :: [msg] -> msg -> [msg]
send obj msg | {obj = msg:_obj1} = _obj1
-- Client process of an bank account
client s | {_s1 = send s (Balance _b)} =
  if _b==50 then {_s1=[]}  -- stop
            else if _b>50 then {client (send _s1 (Withdraw 30))} -- buy
                          else {client (send _s1 (Deposit 70))} -- work

We start the account and client process with an initial amount of 100:

     {make_account S, client (send S (Deposit 100))}

A Curry system evaluates this goal by a concurrent evaluation of both processes and computes the final answer

     {S=[Deposit 100, Balance 100, Withdraw 30, Balance 70, Withdraw 30,
         Balance 40, Deposit 70, Balance 110, Withdraw 30, Balance 80,
         Withdraw 30, Balance 50]}

which shows the different messages sent to the account process.

B Standard Prelude

This section contains the standard prelude for Curry programs. This prelude will be imported to every Curry program, i.e., the names declared in the prelude cannot be redefined.

To do: The definition is still incomplete and will be extended.

-- Infix operator declarations
infixl 7 *, /, `div`, `mod`
infixl 6 +, -
infixr 5 ++
infix  4 ==, <, >, <=, >=
infixr 3 &&, /\
infixr 2 ||
infixr 1 >>, >>=

-- Boolean values
data Bool = True | False
-- Sequential conjunction
(&&)              :: Bool -> Bool -> Bool
(&&)              eval rigid
True  && x        = x
False && _= False
-- Sequential disjunction
(||)              :: Bool -> Bool -> Bool
(||)              eval rigid
True  || _= True
False || x        = x
-- Negation
not               :: Bool -> Bool
not               eval rigid
not True          = False
not False         = True

-- Pairs
data (a,b) = (a,b)

fst               :: (a,b) -> a
fst (x,_)         = x
snd               :: (a,b) -> b
snd (_,y)         = y

-- Unit type
data () = ()

-- Lists
data [a] = [] | a : [a]
head              :: [a] -> a
head (x:_)        = x
tail              :: [a] -> [a]
tail (_:xs)       = xs
-- Concatenation
(++)              :: [a] -> [a] -> [a]
[]     ++ ys      = ys
(x:xs) ++ ys      = x : xs++ys
-- List length
length            :: [a] -> Int
length []         = 0
length (_:xs)     = 1 + length xs
-- Map a function on a list
map               :: (a->b) -> [a] -> [b]
map _[]          = []
map f (x:xs)      = f x : map f xs
-- Accumulate all list elements
foldr             :: (a->b->b) -> b -> [a] -> b
foldr _z []      = z
foldr f z (x:xs)  = f x (foldr f z xs)
-- Filter elements in a list
filter            :: (a -> Bool) -> [a] -> [a]

filter _[]       = []
filter p (x:xs)   = if p x then x : filter p xs
                           else filter p xs
-- Join two lists to one list of pairs
zip               :: [a] -> [b] -> [(a,b)]
zip []     []     = []
zip (x:xs) (y:ys) = (x,y) : zip xs ys
-- Concatenate a list of lists into one list
concat   :: [[a]] -> [a]
concat l =  foldr (++) [] l
-- return prefix of length n
take     :: Int -> [a] -> [a]
take n l = if n==0 then [] else takep n l
   where takep _[]     = []
         takep n (x:xs) = x : take (n-1) xs
-- return suffix without first n elements
drop     :: Int -> [a] -> [a]
drop n l = if n==0 then l else dropp n l
   where dropp _[]     = []
         dropp n (_:xs) = drop (n-1) xs
-- return longest prefix with elements satisfying a predicate
takeWhile          :: (a -> Bool) -> [a] -> [a]
takeWhile _[]     = []
takeWhile p (x:xs) = if p x then x : takeWhile p xs else []
-- return suffix without takeWhile prefix
dropWhile          :: (a -> Bool) -> [a] -> [a]
dropWhile _[]     = []
dropWhile p (x:xs) = if p x then dropWhile p xs else x:xs

-- Conversion functions between characters and their ASCII values
ord :: Char -> Int
chr :: Int -> Char

-- Convert a term into a printable representation

show :: a -> String

-- Types of primitive arithmetic functions and predicates
(+)   :: Int -> Int -> Int
(-)   :: Int -> Int -> Int
(*)   :: Int -> Int -> Int
div   :: Int -> Int -> Int
mod   :: Int -> Int -> Int
(<)   :: Int -> Int -> Bool
(>)   :: Int -> Int -> Bool
(<=)  :: Int -> Int -> Bool
(>=)  :: Int -> Int -> Bool

-- Monadic IO
data IO a  -- conceptually: World -> (a,World)
(>>)              :: IO a -> IO b        -> IO b
(>>=)             :: IO a -> (a -> IO b) -> IO b
putChar           :: Char -> IO ()
getChar           :: IO Char
done              :: IO ()
return            :: a -> IO a
readFile          :: String -> IO String
writeFile         :: String -> String -> IO ()
putStr            :: String -> IO ()
putStr []         = done
putStr (c:cs)     = putChar c >> putStr cs
putStrLn          :: String -> IO ()
putStrLn cs       = putStr cs >> putChar '\n'
getLine           :: IO String
getLine           = getChar >>= \c ->
                    if c=='\n' then return []
                               else getLine >>= \cs -> return (c:cs)

-- Encapsulated search

-- primitive operator to control non-determinism
try :: (a->Constraint) -> [a->Constraint]
-- compute all solutions via depth-first search
all           :: (a->Constraint) -> [a->Constraint]
all g         = collect (try g)
              where collect []         = []
                    collect [g]        = g
                    collect (g1:g2:gs) = concat (map all (g1:g2:gs))
-- compute first solution via depth-first search
once          :: (a->Constraint) -> (a->Constraint)
once g        = head (all g)
-- compute all values of solutions via depth-first search
findall       :: (a->Constraint) -> [a]
findall g     = unpack (all g)
-- compute best solution via branch-and-bound with depth-first search
best          :: (a->Constraint) -> (a->a->Bool) -> [a->Constraint]
-- compute one solution with a fair search
one           :: (a->Constraint) -> [a->Constraint]
-- compute one solution with a fair search satisfying a condition
condSearch    :: (a->Constraint) -> (a->Bool) -> [a->Constraint]
-- show the solution of a solved constraint
browse        :: (a->Constraint) -> IO ()
-- show the solutions of a list of solved constraints
browseList    :: [a->Constraint] -> IO ()
browseList []     = done
browseList (g:gs) = browse g >> putChar '\n' >> browseList gs.

-- unpack the solution's values from a list of solutions
unpack        :: [a->Constraint] -> [a]
unpack []     = []
unpack (g:gs) | {g x} = x : unpack gs  where x free

C Syntax of Curry

The syntax is still preliminary and not intended to be used by automatic tools. Nevertheless, it provides a precise definition of the concrete syntax which can be further discussed.

The syntax is close to Haskell but the following differences should be noted.

• As-patterns are missing

• Case expressions are missing

• Currently, there are no infix constructors except for “:”, the predefined list consstructor. They will be added later, although they are already used in concrete example programs.

C.1 Lexicon

The case of identifiers matters, i.e., “abc” differs from “Abc”. There are four case modes selectable at compilation time:

• Prolog mode: variables start with an upper case latter, all other identifier symbols start with a lower case letter.

• Gödel mode: like Prolog mode with the cases swapped.

• Haskell mode: see section 1.3 of the Haskell report.

• free: no constrains on the case of identifiers.

The default case mode is free. If a case mode is selected but not obeyed, the compiler issues a warning.

The syntax does not define the following non-terminal symbols defining classes of identifiers: ModuleID, TypeConstrID, DataConstrID, TypeVarID, InfixOpID, FunctionID, VariableID. All, except InfixOpID, consist of an initial letter, whose upper or lower case depend on the case mode, followed by any number of letters, digits, and/or underscores. Additionally, VariableID can also start with an underscore and ModuleID can contain dots at inner positions. InfixOpID is any string of characters from the string “~!@#$%^&*+-=<>?./|” or another identifier (like VariableID) enclosed in `…` like `mod`.

The syntax leaves undefined BasicExpr of primitive types. These are literal constants, such as “1”, “True”, or the character “'a'”. They are as in Java. Java, in constrast to Haskell, adopts the Unicode standard to represent characters and character strings.

Comments begins either with “--” and terminate at the end of the line or with “{-” and terminate with a matching “-}”, i.e., the delimiters “{-” and “-}” act as parentheses and can be nested.

C.2 Layout

To do: Describe layout rules (similarly to Haskell)

C.3 Context Free Syntax

Module ::= module ModuleID [Exports] where Block ModuleID ::= see lexicon

Exports ::= ( Export_{1} , … Export_{n} ) Export ::= FunctionName

| TypeConstrID | TypeConstrID ( DataConstrID_{1} , … DataConstrID_{n} ) | TypeConstrID (..) | module ModuleID [( FuncOrType_{1} , … FuncOrType_{n} )]

FuncOrType ::= FunctionName | TypeConstrID

Block ::= { [Import_{1} ; … Import_{n} [;]] n ⩾ 0 [Pragma_{1} ; … Pragma_{n} [;]] n ⩾ 0 [FixityDeclaration_{1} ; … FixityDeclaration_{n} [;]] n ⩾ 0 BlockDeclaration_{1} ; … BlockDeclaration_{m} [;] } m ⩾ 0

Import ::= import ModuleID [( FuncOrType_{1} , … FuncOrType_{n} )] [Renamings] Renamings ::= {Renaming_{1} ; … Renaming_{n} [;] } Renaming ::= renaming FunctionName to FunctionName

| renaming TypeConstrID to TypeConstrID

Pragma ::= pragma PragmaOption

PragmaOption ::= flex | rigid | optmatch

BlockDeclaration ::= DataDeclaration

| FunctionDeclaration

DataDeclaration ::= data {TypeDeclaration_{1} ; … TypeDeclaration_{n} [;] } n > 0 TypeDeclaration ::= TypeConstrID TypeVarID_{1} … TypeVarID_{n} n ⩾ 0

= ConstrDeclaration_{1} | … ConstrDeclaration_{m} m > 0

TypeConstrID ::= see lexicon ConstrDeclaration ::= DataConstrID TypeExpr_{1} … TypeExpr_{n} n ⩾ 0

DataConstrID ::= see lexicon

TypeExpr ::= QTypeConstrID TypeExpr_{1} … TypeExpr_{n} n ⩾ 0 | TypeVarID

| ()

| ( TypeExpr ) | ( TypeExpr_{1} , … TypeExpr_{n} ) n > 1 | [ TypeExpr ] | TypeExpr -> TypeExpr

| Bool | Int | Char | String | Float

TypeVarID ::= see lexicon FixityDeclaration ::= FixityKeyword {FixityArgument_{1} ; … FixityArgument_{n} [;] } n > 0

FixityKeyword ::= infixl | infixr | infix FixityArgument ::= Natural InfixOpID_{1} , … InfixOpID_{n} n > 0

Natural ::= Digit | Digit Natural

Digit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 InfixOpID ::= see lexicon FunctionDeclaration ::= [Signature] [EvalAnnot] Equat_{1} … Equat_{n} n > 0

Signature ::= FunctionName :: FunctionType FunctionName ::= ( InfixOpID )

| FunctionID

FunctionID ::= see lexicon EvalAnnot ::= FunctionName eval Annotation Annotation ::= flex

| rigid

| EvalTree

EvalTree ::= Position : Branch

| rule

| EvalTree or EvalTree

Position ::= Natural

| Natural . Position

Branch ::= flex ( ConsTree_{1} , … ConsTree_{n} ) n > 0

| rigid ( ConsTree_{1} , … ConsTree_{n} ) n > 0

ConsTree ::= QConstrID => EvalTree

Equat ::= FunctionName Pattern = Expr [where LocalDefs]

| FunctionName Pattern CondExpr [where LocalDefs]

Pattern ::= ConstrTerm_{1} … ConstrTerm_{n} n ⩾ 0 ConstrTerm ::= VariableID |

| QDataConstrID

| ()

| ( ConstrTerm_{1} , … ConstrTerm_{n} ) n > 1 | ( QDataConstrID ConstrTerm_{1} … ConstrTerm_{n} ) n > 0 | ( ConstrTerm : ConstrTerm ) | [ ConstrTerm_{1} , … ConstrTerm_{n} ] n ⩾ 0

VariableID ::= see lexicon LocalDefs ::= {ValueDeclaration_{1} ; … ValueDeclaration_{n} [;] } n > 0

ValueDeclaration ::= FunctionDeclaration | PatternDeclaration | VariableID_{1} , … VariableID_{n} free n ⩾ 0

PatternDeclaration ::= ConstrTerm = Expr [where LocalDefs]

CondExpr ::= | Expr = Expr [CondExpr]

Expr ::= \ Pattern -> Expr | let LocalDefs in Expr | if Expr then Expr else Expr | Expr InfixOpID Expr | Constraint | ChoiceExpr | FunctExpr

Constraint ::= { Expr_{1} , … Expr_{n} } n ⩾ 0 ChoiceExpr ::= choice {ChoiceBranch_{1} ; … ChoiceBranch_{n} [;] } n ⩾ 0

ChoiceBranch ::= Expr -> Expr [where LocalDefs] FunctExpr ::= [FunctExpr] BasicExpr BasicExpr ::= QVariableID

                   | ()

| ( Expr )

| ( Expr_{1} , … Expr_{n} ) n > 1 | [ Expr_{1} , … Expr_{n} ] n ⩾ 0 | Bool | Int | Char | String | Float

QTypeConstrID ::= ModuleId . TypeConstrID | TypeConstrID QDataConstrID ::= ModuleId . DataConstrID | DataConstrID QVariableID ::= ModuleId . VariableID | VariableID

Bool ::= see lexicon Int ::= see lexicon Char ::= see lexicon String ::= see lexicon Float ::= see lexicon

In CondExpr and ChoiceBranch, the first expression must have type Constraint or Bool. In the latter case, a Boolean expression b in a condition is considered as an abbreviation for the constraint

{b=True}.

Not all evaluation annotations generated by EvalAnnot are valid, since the structure of the annotations must be compatible with the structure of the rules. In particular, each position must be a position of a constructor in some left-hand side of the rule, and positions must be nested, i.e., in an annotation of the form A(⋯=>p.i), the “parent” position p must occur in A. The evaluation annotations are a convenient syntactic presentation of definitional trees, which are formalized in Appendix D and form the basis of the operational semantics of Curry.

D Operational Semantics of Curry

The precise specification of the operational semantics of Curry is based on the evaluation annotations for each function. Therefore, we describe the computation model by providing a precise definition of the evaluation annotations (Section D.1) which is the basis to define the computation steps on expressions (Section D.2). The extension of this basic computation model to conditional rules, solving equational constraints, and higher-order functions is described in Sections D.3, D.4 and D.5. Section D.6 describes the automatic generation of evaluation annotations if they are omitted by the programmer. Finally, Section D.7 specifies the operational semantics of the primitive operator try for encapsulating search.

D.1 Definitional Trees

We start by considering only the unconditional first-order part of Curry, i.e., rules do not contain conditions and λ-abstractions and partial function applications are not allowed. We assume some familiarity with basic notions of term rewriting [14] and functional logic programming [19].

We denote by C the set of constructors (with elements c, d), by F the set of defined functions or operations (with elements f, g), and by X the set of variables (with elements x, y), where C, F and X are disjoint. An expression (data term) is a variable x ∈ X or an application φ(e_{1}, …, e_{n}) where φ ∈ C ∪ F (φ ∈ C) has arity n and e_{1}, …, e_{n} are expressions (data terms).^{10} The set of all expressions and data terms are denoted by T (C ∪ F, X) and T (C, X), respectively. A pattern is an expression of the form f(t_{1}, …, t_{n}) where each variable occurs only once, f ∈ F is an n-ary function, and t_{1}, …, t_{n} ∈ T (C, X). root(e) denotes the symbol at the root of the expression e. A position p in an expression e is represented by a sequence of natural numbers, e|_{p} denotes the subterm or subexpression of e at position p, and e[e′]_{p} denotes the result of replacing the subterm e|_{p} by the expression e′ (see [14] for details).

A substitution is a mapping σ: X → T (C ∪ F, X) with σ(x) ≠ x only for finitely many variables x. Thus, we denote a substitution by σ = {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}}, where σ(x_{i}) ≠ x_{i} for i = 1, …, n, and id denotes the identity substitution (n = 0). Dom(σ) = {x_{1}, …, x_{n}} is the domain of σ and

VRan(σ) = {x | x is a variable occurring in some t_{i}, i ∈ {1, …, n}}

is its variable range. Substitutions are extended to morphisms on expressions by σ(f(e_{1}, …, e_{n})) = f(σ(e_{1}), …, σ(e_{n})) for every expression f(e_{1}, …, e_{n}).

A Curry program is a set of rules l = r satisfying some restrictions (see Section 2.2). In particular, the left-hand side l must be a pattern. A rewrite rule is called a variant of another rule if it is obtained by a unique replacement of variables by other variables.

An answer expression is a pair σ e consisting of a substitution σ (the answer computed so far) and an expression e. An answer expression σ e is solved if e is a data term. We sometimes omit the identity substitution in answer expressions, i.e., we write e instead of id e if it is clear from the context. A disjunctive expression is a (multi-)set of answer expressions {σ_{1} e_{1}, …, σ_{n} e_{n}}. The set of all disjunctive expressions is denoted by D.

10Since we do not consider partial applications in this part, we write the full application as φ(e_{1}, …, e_{n}) which is equivalent to Curry’s notation φ e_{1} … e_{n}.

A single computation step performs a reduction in exactly one unsolved expression of a disjunction. To provide a precise definition of the operational semantics, we use definitional trees.^{11} A definitional tree is a hierarchical structure containing all rules of a defined function. T is a definitional tree with pattern π iff the depth of T is finite and one of the following cases holds:

T = rule(l = r), where l = r is a variant of a rule such that l = π.

T = branch(π, o, r, T_{1}, …, T_{k}), where o is an occurrence of a variable in π, r ∈ {rigid, flex}, c_{1}, …, c_{k} are different constructors of the sort of π|_{o}, for some k > 0, and, for all i = 1, …, k, T_{i} is a definitional tree with pattern π[c_{i}(x_{1}, …, x_{n})]_{o}, where n is the arity of c_{i} and x_{1}, …, x_{n} are new variables.

T = or(T_{1}, T_{2}), where T_{1} and T_{2} are definitional trees with pattern π.^{12}

A definitional tree of an n-ary function f is a definitional tree T with pattern f(x_{1}, …, x_{n}), where x_{1}, …, x_{n} are distinct variables, such that for each rule l = r with l = f(t_{1}, …, t_{n}) there is a node rule(l′ = r′) in T with l variant of l′. In the following, we write pat(T ) for the pattern of a definitional tree T .

It is always possible to construct a definitional tree for each function (concrete algorithms are described in [3, 30] and in Section D.6). For instance, consider the following definition of the less-or-equal predicate on natural numbers represented by data terms built from z (zero) and s (successor):

     data Nat = z | s Nat
     leq :: Nat -> Nat -> Bool
     leq z     n     = True
     leq (s m) z     = False
     leq (s m) (s n) = leq m n

Consider a function call like (leq e_{1} e_{2}). In order to apply some reduction rule, the first argument e_{1} must always be evaluated to head normal form (i.e., to an expression without a defined function symbol at the top). However, the second argument must be evaluated only if the first argument has the form (s e).^{13} This dependency between the first and the second argument is expressed by the definitional tree

branch(leq(x_{1}, x_{2}), 1, flex,rule(leq(z, x_{2}) =True),
branch(leq(s(x), x_{2}), 2, flex,rule(leq(s(x), z) =False),
rule(leq(s(x), s(y)) =leq(x, y))))

which corresponds to the explicit evaluation annotation

     leq eval 1:flex(0 => rule, s => 2:flex(0 => rule, s => rule))

11Our notion is influenced by Antoy’s work [3], but here we use an extended form of definitional trees.

12For the sake of simplicity, we consider only binary or nodes. The extension to such nodes with more than two subtrees is straightforward.

13Naive lazy narrowing strategies may also evaluate the second argument in any case. However, as shown in [5], the consideration of dependencies between arguments is essential to obtain optimal evaluation strategies.

Computation step for a single expression:

\frac{Eval[[e]] ⇒ D}{Eval[[\{\} ∧ e]] ⇒ D}  \frac{Eval[[e]] ⇒ D}{Eval[[e ∧ \{\}]] ⇒ D}  \frac{Eval[[e_{i}]] ⇒ D}{Eval[[e_{1} ∧ e_{2}]] ⇒ replace(e_{1} ∧ e_{2}, i, D)} i ∈ \{1, 2\}
\frac{Eval[[e_{i}]] ⇒ D}{Eval[[c(e_{1}, …, e_{n})]] ⇒ replace(c(e_{1}, …, e_{n}), i, D)} i ∈ \{1, …, n\}
\frac{Eval[[f(e_{1}, …, e_{n}); T ]] ⇒ D}{Eval[[f(e_{1}, …, e_{n})]] ⇒ D} if T is a definitional tree for f with fresh variables

Computation step for an operation-rooted expression e:

\overline{Eval[[e; rule(l = r)]] ⇒ \{id σ(r)\}} if σ is a substitution with σ(l) = e

\frac{Eval[[e; T_{1}]] ⇒ D_{1} Eval[[e; T_{2}]] ⇒ D_{2}}{Eval[[e; or(T_{1}, T_{2})]] ⇒ D_{1} ∪ D_{2}}

Eval[[e; branch(π, p, r, T_{1}, …, T_{k})]] ⇒

D  if e|_{p} = c(e_{1}, …, e_{n}), pat(T_{i})|_{p} = c(x_{1}, …, x_{n}), and Eval[[e; T_{i}]] ⇒ D
∅  if e|_{p} = c(⋯) and pat(T_{i})|_{p} ≠ c(⋯), i = 1, …, k
⋃_{i=1}^{k}{σ_{i} σ_{i}(e)} if e|_{p} = x, r = flex, and σ_{i} = {x ↦ pat(T_{i})|_{p}}
replace(e, p, D) if e|_{p} = f(e_{1}, …, e_{n}) and Eval[[e|_{p}]] ⇒ D

Derivation step for a disjunctive expression:

\frac{Eval[[e]] ⇒ \{σ_{1} e_{1}, …, σ_{n} e_{n}\}}{\{σ e\} ∪ D ⇒ \{σ_{1} ∘ σ e_{1}, …, σ_{n} ∘ σ e_{n}\} ∪ D}

Figure 1: Operational semantics of Curry

This definitional tree or annotation specifies that the first argument is initially evaluated and the second argument is only evaluated if the first argument has the constructor s at the top. The precise operational meaning induced by definitional trees is described in the following section.

D.2 Computation Steps

The operational semantics is defined by the derivability relation D_{1} ⇒ D_{2} on disjunctive expressions

specified in Figure 1. An inference rule \frac{α}{β} should be read as “if α is derivable, then β is also

derivable”. We say that the computation of an expression e suspends if there is no D with Eval[[e]] ⇒ D. For the purpose of this definition, we interpret a constraint {e_{1},...,e_{n}} as an expression of the form e_{1} ∧…∧e_{n} where ∧ is a binary infix operator (the concurrent conjunction of two constraints). A constraint is solvable if it can be reduced to {}. The exact method to solve constraints depends on the constraint solver. A method to solve equational constraints on data terms is specified in Section D.4.

As can be seen by the rules for evaluating constraints in Figure 1, the concurrent conjunction of two constraints is evaluated by applying computation steps to one of the two constraints. Since both constraints must be finally solved (i.e., reduced to {}), one can consider the evaluation of a concurrent conjunction as two computation threads evaluating these constraints. They are synchronized by accessing common variables (which may suspend a thread, see below). In a simple sequential implementation, the evaluation of e_{1} ∧ e_{2} could be started by an attempt to solve e_{1}. If the evaluation of e_{1} suspends, an evaluation step is applied to e_{2}. If a variable responsible to the suspension of e_{1} is instantiated, the left expression e_{1} will be evaluated in the subsequent step. Thus, we obtain a concurrent behavior with an interleaving semantics. However, a sophisticated implementation should provide a fair selection of threads, e.g., as done in a Java-based implementation of Curry [23].

A computation step for an expression e attempts to apply a reduction step to an outermost operation-rooted subterm in e by evaluating this subterm with the definitional tree for the function symbol at the root of this subterm. Although it is unspecified which outermost subterm is evaluated, we assume that a single (e.g., leftmost) outermost subterm is always selected. The evaluation of an operation-rooted term is defined by a case distinction on the definitional tree. If it is a rule node, this rule is applied. An or node produces a disjunction where the different alternatives are combined. Note that the entire disjunction suspends if one disjunct suspends, which is necessary to ensure completeness [21]. For a similar reason, we cannot commit to a disjunct which does not bind variables but we have to consider both alternatives (see [6] for a counter-example). The most interesting case is a branch node. Here we have to branch on the value of the top-level symbol at the selected position. If the symbol is a constructor, we proceed with the appropriate definitional subtree, if possible. If it is a function symbol, we proceed by evaluating this subexpression. If it is a variable and the branch is flexible, we instantiate the variable to the different constructors, otherwise (if the branch is rigid) we cannot proceed and suspend. The auxiliary function replace puts a possibly disjunctive expression into a subterm:

replace(e, p, {σ_{1} e_{1}, …, σ_{n} e_{n}}) = {σ_{1} σ_{1}(e)[e_{1}]_{p}, …, σ_{n} σ_{n}(e)[e_{n}]_{p}} (n ≥ 0)

The overall computation strategy on disjunctive expressions takes a disjunct σ e not in solved form and evaluates e. If the evaluation does not suspend and yields a disjunctive expression, we substitute it for σ e composed with the old answer substitution. Soundness and completeness results for the operational semantics can be found in [21]. Note that the evaluation of expressions is completely deterministic if the concurrent conjunction of constraints does not occur.

D.3 Conditional Rules

Following the approach taken in Babel [34], we can easily extend our operational semantics to conditional rules by considering a conditional rule “l | {c} = r” as syntactic sugar for the rule l = (c ⇒ r), where the right-hand side is a guarded expression. The operational meaning of a guarded expression “c ⇒ r” is defined by the predefined rule

     ({} ⇒ x)  =  x .

Thus, a guarded expression is evaluated by an attempt to solve the condition. If the condition c is solvable, the guarded expression c ⇒ r is replaced by r, i.e., by the right-hand side of the conditional rule. If the condition is not solvable and does not suspend, the disjunct containing this guarded expression will be deleted by the definition of computation steps, i.e., the application of the conditional rule fails and does not contribute to the final result.

\frac{Eval[[e_{i}]] ⇒ D}{Eval[[e_{1}=e_{2}]] ⇒ replace(e_{1}=e_{2}, i, D)} if e_{i} = f(t_{1}, …, t_{n}), i ∈ \{1, 2\}

\overline{Eval[[c(e_{1}, …, e_{n})=c(e′_{1}, …, e′_{n})]] ⇒ \{id e_{1}=e′_{1} ∧ … ∧ e_{n}=e′_{n}\}}

\overline{Eval[[c(e_{1}, …, e_{n})=d(e′_{1}, …, e′_{m})]] ⇒ ∅} if c ≠ d or n ≠ m

\frac{Eval[[x=e]] ⇒ D}{Eval[[e=x]] ⇒ D}

\overline{Eval[[x=y]] ⇒ \{\{x ↦ y\} \{\}\}}

Eval[[x=c(e_{1}, …, e_{n})]] ⇒ {{x ↦ c(y_{1}, …, y_{n})} {y_{1}=e_{1} ∧ … ∧ y_{n}=e_{n}}} if x ∉ cv(c(e_{1}, …, e_{n})), y_{1}, …, y_{n} fresh variables

\overline{Eval[[x=c(e_{1}, …, e_{n})]] ⇒ ∅} if x ∈ cv(c(e_{1}, …, e_{n}))

Figure 2: Solving equational constraints

D.4 Equational Constraints

An equational constraint e_{1}=e_{2} is solvable if both sides are reducible to a unifiable data term (strict equality). An equational constraint can be solved in an incremental way by an interleaved lazy evaluation of the expressions and binding of variables to constructor terms. The evaluation steps implementing this method are shown in Figure 2, where we consider the symbol = is a binary infix function symbol. The last two rules implements an occur check where the critical variables (cv) are only those variables occurring outside a function call:

cv(x) = {x}
cv(c(e_{1}, …, e_{n})) = cv(e_{1}) ∪ … ∪ cv(e_{n})
cv(f(e_{1}, …, e_{n})) = ∅

However, Curry implementations can also provide other methods to solve equational constraints or other types of constraints with appropriate constraint solvers. The only property, which is important for the operational semantics, is the fact that a solved constraint has the form {}, i.e., a solvable constraint c is reducible to the answer expression σ {} where σ is a solution of c.

D.5 Higher-Order Features

Warren [46] has shown for the case of logic programming that the higher-order features of functional programming can be implemented by providing a (first-order) definition of the application function. Since Curry supports the higher-order features of current functional languages but excludes the guessing of higher-order objects by higher-order unification (as, e.g., in [22, 35, 40]), the operational semantics specified in Figure 1 can be simply extended to cover Curry’s higher-order features by adding the following axiom (here we denote by the infix operator “@” the application of a function to an expression):

Eval[[φ(e_{1}, …, e_{m})@e]] ⇒ φ(e_{1}, …, e_{m}, e) if φ has arity n and m < n

Thus, we evaluate an application by simply adding the argument to a partial application. If a function has the right number of arguments, it is evaluated by the rules in Figure 1. Note that the function application is “rigid” in its first argument since the application suspends if the applied function is unknown (instead of a possible but expensive non-deterministic search for the appropriate function).

λ-abstractions occurring in expressions are anonymous functions and can be implemented by assigning a new name to each λ-abstraction, where the free variables become parameters of the function. For instance, the λ-abstraction (f is a free variable)

     \x y -> f x y + 2

can be replaced by the (partial) application (lambda f), where lambda is a new name, and adding the rule

     lambda f x y = f x y + 2

Note that this transformation (as well as the extension of Eval[[·]] above) is only used to explain the operational meaning of Curry’s higher-order features. A concrete Curry system is free to choose other implementation techniques.

D.6 Generating Definitional Trees

Curry’s computation model is based on the specification of a definitional tree for each operation. Although definitional trees are a high-level formalism to specify evaluation strategies, it is tedious to annotate each operation which its definitional tree. Therefore, the user can omit them. In this case, they are automatically inserted by the Curry system. In the following, we present Curry’s algorithm to generate definitional trees from the left-hand sides of the functions’ rules.

The generation of definitional trees for each function is not straightforward, since there may exist many non-isomorphic definitional trees for a single function representing different evaluation strategies. This demands for a default strategy to generate definitional trees. Curry uses the following default strategy:

1. Pattern-matching is performed from left to right.

2. or nodes are generated in case of a conflict between constructors and variables, i.e., if two rules have a variable and a constructor at the same position on the left-hand side.

This default strategy is reasonable since it does not generate any or node for most typical functional programs and is also used in current functional languages [45]. However, there are programs where this default does not generate the best possible results (see below).

To specify the algorithm, we define by

DP (π, R) = {o position of a variable in π | root(l|_{o}) ∈ C for some l = r ∈ R} the set of demanded positions of a pattern π w.r.t. a set of rules R. For instance, the demanded positions of the pattern leq(x,y) w.r.t. the rules for the predicate leq (see Section D.1, page 45) are {1, 2} referring to the pattern variables x and y. The generation of a definitional tree for a pattern π and a set of rules R (where l is an instance of π for each l = r ∈ R) is described by the function gt(π, m, R) (m ∈ {flex, rigid} determines the mode annotation in the generated branch nodes). We distinguish the following cases for gt:

1. If the position o is leftmost in DP (π, R), {root(l|_{o}) | l = r ∈ R} = {c_{1}, …, c_{k}} where c_{1}, …, c_{k} are different constructors with arities n_{1}, …, n_{k}, and R_{i} = {l = r ∈ R | root(l|_{o}) = c_{i}}, then

gt(π, m, R) = branch(π, o, m, gt(π[c_{1}(x_{11}, …, x_{1n_{1}})]_{o}, m, R_{1}),
…,
gt(π[c_{k}(x_{k1}, …, x_{kn_{k}})]_{o}, m, R_{k}))

where x_{ij} are fresh variables. I.e., if all rules have a constructor at the leftmost demanded position, we generate a branch node.

2. If the position o is leftmost in DP (π, R) and R′ = {l = r ∈ R | root(l|_{o}) ∈ C} ≠ R, then

gt(π, m, R) = or(gt(π, m, R′), gt(π, m, R − R′))

I.e., we generate an or node if the leftmost demanded position of the pattern is not demanded by the left-hand sides of all rules.

3. If DP (π, R) = ∅ and l = r variant of some rule in R with l = π, then

gt(π, m, R) = rule(l = r)

Note that all rules in R are variants of each other if there is no demanded position (this follows from the weak orthogonality of the rewrite system). For non-weakly orthogonal rewrite systems, which may occur if non-deterministic functions are allowed [17] or conditional rules are transformed into unconditional rules (see Section D.3), the rules in R may not be variants. In this case we simply connect the different rules by or nodes.

If R is the set of all rules defining the n-ary function f, then a definitional tree for f is generated by computing gt(f(x_{1}, …, x_{n}), m, R), where m = flex if the type of f has the form ⋯->Bool, i.e., if f denotes a predicate, and m = rigid otherwise (this default can be changed by the pragmas “flex” and “rigid”, see Section 9).

It is easy to see that this algorithm computes a definitional tree for each function since the number of rules is reduced in each recursive call and it keeps the invariant that the left-hand sides of the current set of rules are always instances of the current pattern.

The algorithm gt conforms to the evaluation strategy of functional languages like Haskell or Miranda, since it generates for the rules

     f 0 0 = 0
     f x 1 = 0

Eval[[try(g)]] ⇒
[]  if Eval[[c]] ⇒ ∅
[g′]  if Eval[[c]] ⇒ {σ {}} (i.e., σ is a mgu for all equations in c) with
Dom(σ) ⊆ {x, x_{1}, …, x_{n}} (or c = {} and σ = id) and
g′ = \x->let x_{1}, …, x_{n} free in {σ ∘ φ {}}
D  if Eval[[c]] ⇒ {σ {c′}} with Dom(σ) ⊆ {x, x_{1}, …, x_{n}},
g′ = \x->let x_{1}, …, x_{n}, y_{1}, …, y_{m} free in {σ ∘ φ c′}
where y_{1}, …, y_{m} = VRan(σ) \ ({x, x_{1}, …, x_{n}} ∪ free(g)),
and Eval[[try(g′)]] ⇒ D
[g_{1},...,g_{k}] if Eval[[c]] ⇒ {σ_{1} {c_{1}}, …, σ_{k} {c_{k}}}, k > 1, and, for i = 1, …, k,
Dom(σ_{i}) ⊆ {x, x_{1}, …, x_{n}} and
g_{i} = \x->let x_{1}, …, x_{n}, y_{1}, …, y_{m_{i}} free in {σ_{i} ∘ φ c_{i}}
where y_{1}, …, y_{m_{i}} = VRan(σ_{i}) \ ({x, x_{1}, …, x_{n}} ∪ free(g))

Figure 3: Operational semantics of the try operator for g = \x->let x_{1}, …, x_{n} free in {φ c}

the definitional tree

or(branch(f(x1,x2), 1, rigid, branch(f(0,x2), 2, rigid, rule(f(0,0) = 0))),
branch(f(x1,x2), 2, rigid, rule(f(x1,1) = 0)))

This tree is not optimal since it has a non-deterministic or node and always requires the evaluation of the first argument (in the first alternative).

We can avoid the generation of or nodes for this function if we relax the strict left-to-right evaluation strategy and select in case 1 of the definition of gt the leftmost position among all those demanded positions where all rules have a constructor in the left-hand side at this position. This algorithm, which is used if the pragma “optmatch” is chosen (see Section 9), generates the following definitional tree:

branch(f(x1,x2), 2, rigid, branch(f(x1,0), 1, rigid, rule(f(0,0) = 0)),

                            rule(f(x1,1) = 0))

In general, the “optmatch” algorithm generates more powerful evaluation strategies than gt since it is ensured that, for ground expressions, normal forms are always computed (if they exists) provided that the definitional trees contain only branch and rule nodes [3]. If the function definitions are uniform in the sense of [45], then gt and optmatch generate identical definitional trees.

D.7 Encapsulated Search

The exact behavior of the try operator is specified in Figure 3. Note that a substitution φ of the form {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}}, computed by evaluating the body of a search goal, must be encoded as a constraint in the new search goal. Therefore, φ is transformed into its equational representation \overline{φ}, where \overline{φ} is a solved constraint of the form \{x_{1}=t_{1},...,x_{n}=t_{n}\}. Hence, a search goal can always be written as try \x->\{\overline{φ}, c\}. Since the solved constraint \overline{φ} does not have to be evaluated again, we use the sugared form try \x->{φ c} where only c is further evaluated. Thus, an initial search goal try \x->{c} is equivalent to try \x->{id c}.

A search goal is solved (second case) if the constraint is solvable without bindings of global variables. In a deterministic step (third case), we apply the try operator again after adding the newly introduced variables to the list of local variables. Note that the free variables occurring in g, denoted by free(g), must not be locally declared because they can appear also outside of g, and therefore they have to be removed from VRan(σ). In a non-deterministic step (fourth case), we return the different alternatives as the result. Note that the evaluation of the try operator suspends if a computation step on the constraint attempts to bind a free variable. In order to ensure that an encapsulated search will not be suspended due to necessary bindings of free variables, the search goal should be a closed expression when a search operator is applied to it, i.e., the search variable is bound by the lambda abstraction and all other free variables are existentially quantified by local declarations.

If one wants to use free variables in a search goal, e.g., for synchronization in systems where concurrency is intensively used, the goal should perform only deterministic steps until all free variables have been bound by another part of the computation. Otherwise, a non-deterministic step could unnecessarily split the search goal. For instance, consider the expression

      try \x -> {y=[x], append x [0,1] = [0,1]}

The computation of y=[x] suspends because y is free. Therefore, a concurrent computation of the conjunction will split the goal by reducing the append expression. However, if y is first bound to [[]] by another thread of the computation, the search goal could proceed deterministically.

To avoid such unnecessary splittings, we can restrict the applicability of the split case and adapt a solution known as stability from AKL [26] and Oz [42]. For this purpose, we can slightly change the definition of try such that non-deterministic steps lead to a suspension as long as a deterministic step might be enabled by another part of the computation, i.e., the search goal contains free global variables. To do so, we have to replace only the fourth rule of the try operator:

Eval[[try(g)]] ⇒ [g_{1},...,g_{k}] if Eval[[c]] ⇒ {σ_{1} {c_{1}}, …, σ_{k} {c_{k}}}, k > 1,
Eval[[c]] ⇏ {σ {c′}}, free(c) ⊆ {x, x_{1}, …, x_{n}}
and, for i = 1, …, k,

g_{i} = \x->let x_{1}, …, x_{n}, y_{1}, …, y_{m_{i}} free in {σ_{i} ∘ φ c_{i}} where y_{1}, …, y_{m_{i}} = VRan(σ_{i}) \ ({x, x_{1}, …, x_{n}} ∪ free(g))

Thus, a non-deteterministic step is only performed if no deterministic step is possible and the unsolved constraint c contains no free variables except those locally declared in the search goal. Global variables appearing in the data terms t_{i} of the substitution φ = {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}} but not in c are not considered by these conditions because they cannot influence the further evaluation of c. Note that the former condition Dom(σ_{i}) ⊆ {x, x_{1}, …, x_{n}} is covered by the new condition free(c) ⊆ {x, x_{1}, …, x_{n}} because Dom(σ_{i}) is always a subset of free(c).

Note that the first definition of try in Figure 3 computes non-deterministic splittings where the latter definition suspends. On the other hand, the latter definition can avoid some unnecessary splittings. Thus, different implementations of Curry can support one or both of these definitions.

References

[1] H. Aït-Kaci. An Overview of LIFE. In J.W. Schmidt and A.A. Stogny, editors, Proc. Workshop on Next Generation Information System Technology, pp. 42–58. Springer LNCS 504, 1990.

[2] H. Aït-Kaci, P. Lincoln, and R. Nasr. Le Fun: Logic, equations, and Functions. In Proc. 4th IEEE Internat. Symposium on Logic Programming, pp. 17–23, San Francisco, 1987.

[3] S. Antoy. Definitional Trees. In Proc. of the 3rd International Conference on Algebraic and Logic Programming, pp. 143–157. Springer LNCS 632, 1992.

[4] S. Antoy. Optimal Non-Deterministic Functional Logic Computations. In Proc. International Conference on Algebraic and Logic Programming (ALP’97), pp. 16–30. Springer LNCS 1298, 1997.

[5] S. Antoy, R. Echahed, and M. Hanus. A Needed Narrowing Strategy. In Proc. 21st ACM Symposium on Principles of Programming Languages, pp. 268–279, Portland, 1994.

[6] S. Antoy, R. Echahed, and M. Hanus. Parallel Evaluation Strategies for Functional Logic Languages. In Proc. of the Fourteenth International Conference on Logic Programming (ICLP’97), pp. 138–152. MIT Press, 1997.

[7] P. Arenas-Sánchez, A. Gil-Luezas, and F.J. López-Fraguas. Combining Lazy Narrowing with Disequality Constraints. In Proc. of the 6th International Symposium on Programming Language Implementation and Logic Programming, pp. 385–399. Springer LNCS 844, 1994.

[8] D. Bert and R. Echahed. Design and Implementation of a Generic, Logic and Functional Programming Language. In Proc. European Symposium on Programming, pp. 119–132. Springer LNCS 213, 1986.

[9] S. Bonnier and J. Maluszynski. Towards a Clean Amalgamation of Logic Programs with External Procedures. In Proc. 5th Conference on Logic Programming & 5th Symposium on Logic Programming (Seattle), pp. 311–326. MIT Press, 1988.

[10] J. Boye. S-SLD-resolution – An Operational Semantics for Logic Programs with External Procedures. In Proc. of the 3rd Int. Symposium on Programming Language Implementation and Logic Programming, pp. 383–393. Springer LNCS 528, 1991.

[11] S. Breitinger, R. Loogen, and Y. Ortega-Mallen. Concurrency in Functional and Logic Programming. In Fuji International Workshop on Functional and Logic Programming. World Scientific Publ., 1995.

[12] M.M.T. Chakravarty, Y. Guo, M. Köhler, and H.C.R. Lock. Goffin - Higher-Order Functions Meet Concurrent Constraints. Science of Computer Programming (to appear), 1997.

[13] L. Damas and R. Milner. Principal type-schemes for functional programs. In Proc. 9th Annual Symposium on Principles of Programming Languages, pp. 207–212, 1982.

[14] N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, pp. 243–320. Elsevier, 1990.

[15] L. Fribourg. SLOG: A Logic Programming Language Interpreter Based on Clausal Superposition and Rewriting. In Proc. IEEE Internat. Symposium on Logic Programming, pp. 172–184, Boston, 1985.

[16] E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel LEAF: A Logic plus Functional Language. Journal of Computer and System Sciences, Vol. 42, No. 2, pp. 139–185, 1991.

[17] J.C. Gonzáles-Moreno, M.T. Hortalá-Gonzáles, F.J. López-Fraguas, and M. Rodríguez-Artalejo. A Rewriting Logic for Declarative Programming. In Proc. ESOP’96, pp. 156–172. Springer LNCS 1058, 1996.

[18] M. Hanus. Compiling Logic Programs with Equality. In Proc. of the 2nd Int. Workshop on Programming Language Implementation and Logic Programming, pp. 387–401. Springer LNCS 456, 1990.

[19] M. Hanus. The Integration of Functions into Logic Programming: From Theory to Practice. Journal of Logic Programming, Vol. 19&20, pp. 583–628, 1994.

[20] M. Hanus. Teaching Functional and Logic Programming with a Single Computation Model. In Proc. Ninth International Symposium on Programming Languages, Implementations, Logics, and Programs (PLILP’97), pp. 335–350. Springer LNCS 1292, 1997.

[21] M. Hanus. A Unified Computation Model for Functional and Logic Programming. In Proc. of the 24th ACM Symposium on Principles of Programming Languages (Paris), pp. 80–93, 1997.

[22] M. Hanus and C. Prehofer. Higher-Order Narrowing with Definitional Trees. In Proc. Seventh International Conference on Rewriting Techniques and Applications (RTA’96), pp. 138–152. Springer LNCS 1103, 1996.

[23] M. Hanus and R. Sadre. A Concurrent Implementation of Curry in Java. In Proc. ILPS’97 Workshop on Parallelism and Implementation Technology for (Constraint) Logic Programming Languages, Port Jefferson (New York), 1997.

[24] P.M. Hill and J.W. Lloyd. The Gödel Programming Language. MIT Press, 1994.

[25] P. Hudak, S. Peyton Jones, and P. Wadler. Report on the Programming Language Haskell (Version 1.2). SIGPLAN Notices, Vol. 27, No. 5, 1992.

[26] S. Janson and S. Haridi. Programming Paradigms of the Andorra Kernel Language. In Proc. 1991 International Logic Programming Symposium, pp. 167–183. MIT Press, 1991.

[27] H. Kuchen, R. Loogen, J.J. Moreno-Navarro, and M. Rodríguez-Artalejo. The Functional Logic Language BABEL and Its Implementation on a Graph Machine. New Generation Computing, Vol. 14, pp. 391–427, 1996.

[28] J.W. Lloyd. Combining Functional and Logic Programming Languages. In Proc. of the International Logic Programming Symposium, pp. 43–57, 1994.

[29] J.W. Lloyd. Declarative Programming in Escher. Technical Report CSTR-95-013, University of Bristol, 1995.

[30] R. Loogen, F. Lopez Fraguas, and M. Rodríguez Artalejo. A Demand Driven Computation Strategy for Lazy Narrowing. In Proc. of the 5th International Symposium on Programming Language Implementation and Logic Programming, pp. 184–200. Springer LNCS 714, 1993.

[31] R. Loogen and S. Winkler. Dynamic Detection of Determinism in Functional Logic Languages. Theoretical Computer Science 142, pp. 59–87, 1995.

[32] F.J. López Fraguas. A General Scheme for Constraint Functional Logic Programming. In Proc. of the 3rd International Conference on Algebraic and Logic Programming, pp. 213–227. Springer LNCS 632, 1992.

[33] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.

[34] J.J. Moreno-Navarro and M. Rodríguez-Artalejo. Logic Programming with Functions and Predicates: The Language BABEL. Journal of Logic Programming, Vol. 12, pp. 191–223, 1992.

[35] G. Nadathur and D. Miller. An Overview of λProlog. In Proc. 5th Conference on Logic Programming & 5th Symposium on Logic Programming (Seattle), pp. 810–827. MIT Press, 1988.

[36] L. Naish. Negation and Control in Prolog. Springer LNCS 238, 1987.

[37] L. Naish. Adding equations to NU-Prolog. In Proc. of the 3rd Int. Symposium on Programming Language Implementation and Logic Programming, pp. 15–26. Springer LNCS 528, 1991.

[38] T. Nipkow. Higher-Order Critical Pairs. In Proc. 6th IEEE Symp. Logic in Computer Science, pp. 342–349. IEEE Press, 1991.

[39] S.L. Peyton Jones and P. Wadler. Imperative Functional Programming. In Proc. 20th Symposium on Principles of Programming Languages (POPL’93), pp. 71–84, 1993.

[40] C. Prehofer. Solving Higher-order Equations: From Logic to Programming. PhD thesis, TU München, 1995. Also appeared as Technical Report I9508.

[41] V.A. Saraswat. Concurrent Constraint Programming. MIT Press, 1993.

[42] C. Schulte and G. Smolka. Encapsulated Search for Higher-Order Concurrent Constraint Programming. In Proc. of the 1994 International Logic Programming Symposium, pp. 505– 520. MIT Press, 1994.

[43] G. Smolka. The Oz Programming Model. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, pp. 324–343. Springer LNCS 1000, 1995.

[44] T. Suzuki, A. Middeldorp, and T. Ida. Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides. In Rewriting Techniques and Applications (RTA’95), pp. 179–193. Springer LNCS 914, 1995.

[45] P. Wadler. Efficient Compilation of Pattern-Matching. In S.L. Peyton Jones, editor, The Implementation of Functional Programming Languages, pp. 78–103. Prentice Hall, 1987.

[46] D.H.D. Warren. Higher-order extensions to PROLOG: are they needed? In Machine Intelligence 10, pp. 441–454, 1982.

Index

Dom, 44 VRan, 44 (), 15 (...) (tuple type), 15 ++, 14 --, 40 ->, 13

/\, 8

:, 14 =, 4, 8 ==, 12 >>, 19

>>=, 19

[], 14

[a] (list type), 14 &&, 12

{-...-}, 40

{...}, 8 _, 7

abstract datatype, 16 accessible

directly, 17 annotation

flexible, 11 rigid, 11

anonymous variable, 7 answer expression, 10, 44 application operator, 49 arity, 4

Bool, 11
Char, 14
choice, 24
chr, 14

comments, 40 committed choice, 24 computation step, 10 condition, 4 conditional equation, 4 conditional rule, 4 confluence, 5 conjunction, 8, 12, 13 concurrent, 8, 13 of constraints, 8 sequential, 12

constant, 4

                                            Constraint, 12

constraint, 8, 12 equational, 8 constructor, 3, 44

data term, 4, 44 ground, 4

datatype abstract, 16 declaration, 3

declaration datatype, 3 export, 16 free, 7 function, 4 import, 17 local, 5, 6 defined function, 3, 44 defining equation, 4 definitional tree, 45 directly accessible, 17 disjunctive expression, 10, 44 domain, 44

entity, 15 exported, 16 imported, 17

equality in constraints, 8 strict, 8, 12, 48 test, 12 equation, 4

conditional, 4 higher-order, 5 equational constraint, 8 evaluation annotation, 11, 43 export declaration, 16 expression, 4, 44

answer, 10, 44 disjunctive, 10, 44 ground, 4

external, 26

external function, 25

False, 11

flex, 11, 27, 50 flexible, 10, 11

Float, 14
free, 7

free declaration, 7 free variable, 5, 6 function

arity, 4 defined, 3, 44 external, 25 non-deterministic, 5

function application, 9, 49 function declaration, 4 function rule, 4

getChar, 19
getLine, 19

ground expression, 4 ground term, 4

head normal form, 45 higher-order equation, 5

import declaration, 17

index, 17
Int, 13

IO, 19

λ-abstraction, 9, 49 left-hand side, 4

let, 6

local declaration, 5, 6

map, 14

module, 15

module, 16

module name, 16 monadic I/O, 19

name

of a module, 16 narrowing, 3, 10 non-deterministic function, 5

not, 12

operation, 3, 44

optmatch, 27, 51
ord, 14

pattern, 44 position, 44

pragma, 26

predicate, 11, 12 prelude, 16 program, 15

putChar, 19
putStr, 19
putStrLn, 19

range, 44 residuation, 3, 10

return, 20

right-hand side, 4 rigid, 10, 11 rigid, 11, 27, 50 root (of an expression), 44 rule, 4

conditional, 4

search goal, 20 search variable, 20

show, 15

solved expression, 44 strict equality, 8, 12, 48

String, 14

subexpression, 44 substitution, 5, 44 subterm, 44 suspended evaluation, 46

True, 11
try, 21

tuple, 15 type constructor, 3 type declaration, 3, 4 type expression, 4 type variable, 4

unbound variable, 6 unit type, 15

variable, 44 anonymous, 7 free, 5, 6 search, 20

variable range, 44 variant, 44

where, 6, 16