Curry

An Integrated Functional Logic Language

Draft of June 6, 1997

Michael Hanus^{1} [editor]

Additional Contributors:

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

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

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

(2) Portland State University, USA, antoy@cs.pdx.edu

(3) RWTH Aachen, Germany, herbert@informatik.rwth-aachen.de

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

Contents

1 Introduction 3

2 Programs 3 2.1 Data Type Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Function Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3 Constraints and Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.4 Higher-order Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

3 Operational Semantics 8

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

5 Modules 14

6 Input/Output 14

7 Choice and Encapsulated Search 16

8 Interface to External Functions and Constraint Solvers 17 8.1 External Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 8.2 External Constraint Solvers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

9 Pragmas 18

10 Interactive Programming Environment 19

A Example Programs 20 A.1 Operations on Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 A.2 Higher-Order Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 A.3 Relational Programming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 A.4 Constraint Solving and Concurrent Programming . . . . . . . . . . . . . . . . . . . . 23 A.5 Concurrent Object-Oriented Programming . . . . . . . . . . . . . . . . . . . . . . . . 25

B Standard Prelude 27

C Syntax of Curry 30 C.1 Lexicon . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C.2 Layout . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C.3 Context Free Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

D Operational Semantics of Curry^{8} 34 D.1 Definitional Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 D.2 Computation Steps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 D.3 Conditional Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 D.4 Higher-Order Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 D.5 Generating Definitional Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

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, higherorder functions, lazy evaluation) and logic programming (logical variables, partial data structures, built-in search). 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 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 [23], SML [30]) 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 [22], λProlog [32]). Therefore, Curry is a strongly typed language with a Hindley/Milner-like polymorphic type system [13].^{1} 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 Data Type Declarations

A data type 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

τ_{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 data type declarations

1The 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.

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

introduces the data type 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.3). 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

Local function declarations are possible by adding where-clauses to the right-hand sides. A whereclause can contain function definitions as well as definitions of constants by pattern matching. The names declared in the where-clauses are only visible in the corresponding right-hand side. For instance, 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

Note that one can define functions with a non-determinate behavior by providing several rules with overlapping left-hand sides or extra-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 [28]). 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^{2} 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 [24].

These conditions ensure the confluence of the rules if they are considered as a conditional term rewriting system [41]. 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 [41] which can be checked instead of the above conditions.

2A 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}}.

Note that defining equations of higher-type, e.g., f = g if f and g are of type Bool -> Bool, are formally excluded to define a simple operational semantics based on first-order rewriting.^{3} 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 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, 31] 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 [27].

Equational constraints should be distinguished from standard Boolean functions since they 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.

If we want to check the equality of two fully known expressions, we can reduce both sides to ground constructor terms and check their identity. This test equality e_{1}==e_{2} checks whether e_{1} and e_{2} are reducible to identical ground data terms. If one of the arguments is a free variable, the test is delayed (i.e., == is “rigid” in both arguments, cf. Section 3). If none of e_{1} and 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

     True  && x = x
     False && x = False

For instance, the test “[0]==[0]” reduces to True, whereas the test “1==0” reduces to False. A test is suspended if one side is a free variable in order to avoid an infinite set of solutions for insufficiently instantiated tests like x==y. Therefore, the test equality can be used where Boolean values are required (e.g., in the condition part of if-then-else), whereas equational constraints can only be applied in the condition of a program rule. In terms of concurrent constraint programming languages [38], == and = correspond to ask and tell equality constraints, respectively. This is also justified by the fact that a test e_{1}==e_{2} is suspended if one side is a variable, whereas an equational constraint e_{1}=e_{2} is checked for satisfiability and propagates new variable bindings.

3Note 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 types may cause a gap between the standard notion of higher-order rewriting and the corresponding equational theory [35].

The different meanings between constraints and test equalities are also shown in their types which are

     (=)  :: a -> a -> Constraint
     (==) :: a -> a -> Bool

(Constraint and Bool denotes the types of Boolean expressions and constraints, respectively, cf. Section 4.1). Usually, strict equalities are only defined on data terms, i.e., = and == are not really polymorphic but overloaded functions. This could be more precisely expressed using type classes which will be considered in a future version.

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 [29], extensions of Curry may provide richer constraint systems to support constraint logic programming applications.

To present a solved constraint to the user, the special constant Valid, denoting the result value of a solved constraint, is used. Thus, the equational constraint [x]=[0] is reduced to the answer expression {x=0}Valid. However, the constant Valid is internal and not available in user programs. In particular, pattern-matching on constraints is not possible.

In order to connect elementary constraints to more complex constraint structures, Curry provides a predefined operation on constraints, the concurrent conjunction /\. If c_{1} and c_{2} are constraints, then c_{1}/\c_{2} is a constraint which is evaluated by solving c_{1} and c_{2} concurrently. In an sequential implementation, c_{1}/\c_{2} can be evaluated by an attempt to solve c_{1}. If the evaluation of c_{1} suspends, an evaluation step is applied to c_{2}. If a variable responsible to the suspension of c_{1} was bound during the last step, the left expression will be evaluated in the subsequent step. Thus, we obtain a concurrent behavior with an interleaving semantics. Formally, the concurrent conjunction could be defined by the single rule

     Valid /\ Valid = Valid

Since both arguments must be solved (reduced to Valid), it is reasonable to evaluate these arguments concurrently.

Syntactically, constraints are always enclosed in curly brackets and the concurrent conjunction can also be written by a comma. Thus, {x = f y, y = h 0} denotes the concurrent conjunction of the equational constraints x = f y and y = h 0.

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.4 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 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 [21, 32, 37]. Since higher-order unification is a computationally expensive operation, Curry delays the application of unknown functions until the function becomes known [2, 40]. 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 [25, 26], Le Fun [2], Life [1], NUE-Prolog [34], or Oz [40]).

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 [31], K-Leaf [16], LPG [8], or SLOG [15]).

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.^{4} Basically, each argument of a function, where a value is demanded by the left-hand sides of the rules, is annotated with a flexible or rigid annotation. If a function call has a free variable at an argument position annotated by rigid, the function call is delayed, otherwise (for flexible arguments) the variable is instantiated to the different constructors in order to apply a rule. For instance, consider the definition of the function f above. Note that the argument is demanded since there are constructors in the left-hand sides of the rules. If f has the evaluation annotation

     f eval 1:flex

(1 denotes the first argument), 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 1: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} Valid

In contrast to logic programming, Curry programs contain nested function calls. Furthermore, the evaluation of some arguments is necessary only if some other arguments are evaluated to particular values. This is demonstrated by 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).^{5} This dependency between the first and the second argument can be expressed by the evaluation annotation

4Evaluation annotations are similar to coroutining declarations [33] 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.

     leq eval 1:flex(s => 2:flex)

which 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. In the general case, we can also specify deeper positions in arguments and non-deterministic selection of arguments in case of overlapping rules (evaluation annotations can be considered as a generalization of definitional trees which have been proposed by Antoy [3] to describe efficient reduction strategies). The general syntax for evaluation annotations can be found in Appendix C.3 and their precise operational meaning is defined in Appendix D.

Note that it is not necessary to specify the evaluation annotations for each function since, similarly to type declarations, they are automatically generated for each function following a leftto-right pattern-matching strategy as in functional languages (see Appendix D.5 for a detailed description). By this default strategy, 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. If one is interested to change this default strategy, one can explicitly write the evaluation annotation for each function.

4 Types

4.1 Built-in Types

The following types are predefined in Curry:

Boolean values: They are predefined by the data type 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

5Naive 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.

     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.

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 by the concurrent conjunction of constraints: /\ is predefined as a left-associative infix operator which solves both arguments concurrently.

     (/\) :: Constraint -> Constraint -> Constraint

Since constraints must always be enclosed in curly brackets, one can also write a comma instead of /\. Thus, {c_{1},c_{2},...,c_{n}} is syntactic sugar for {c_{1}/\c_{2}/\… /\c_{n}}. 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 concurrent conjunction of all constraints of the input list (in order to distinguish elementary constraints from defining equations, constraints are always enclosed in curly brackets where “{}” denotes an empty, i.e., always solvable constraint):

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

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} Valid | {x=2,y=4} Valid

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'].

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]. Each variable, constructor and operation has a unique type, where only the types of constructors have to be declared by data type 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.

To do: Define typing rules.

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

5 Modules

The design of a module system for Curry is not influenced by the functional logic features of Curry. Therefore, the current version of Curry uses a standard module system similar to ALF’s [18] or Gödel’s [22]. The extension to a more sophisticated module system like in SML [30] is a topic for future extensions.

To do: Must be described in more detail.

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 [36] 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 data type 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 Choice and 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 may 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 two independent disjunctions. In order to avoid the splitting of the entire expression and to enable a “don’t care” selection of one element in a disjunction, Curry provides a primitive choice operation of the following form:^{6}

     choice {c_{1}} -> e_{1}

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

where e_{1}, …, e_{n} are of the same type and c_{1}, …, c_{n} are constraints. This expression reduces to some e_{i} where the corresponding constraint is entailed, i.e., if, for some i ∈ {1, …, n}, c_{i} is evaluable to ⋯| σ Valid |⋯ where σ does only bind variables introduced in the choice, then the entire choice expression reduces to the single expression σ(e_{i}).^{7} 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 [20] 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.

6The choice operation is included to provide a very elementary method to encapsulate non-deterministic computations. In a later version, Curry will provide a search operator (similarly to Oz [39]) to give the programmer control on the actions to be taken in non-deterministic situations. In contrast to Oz, it is not necessary to define a function by disjunctions in order to apply search. Thus, the encapsulation of search is initiated by the caller and not visible in the definition of the called functions. This has the advantage that the same function can be used for deterministic evaluation or search depending on the structure of the actual arguments (ground expressions or free variables).

7The choice corresponds to the committed choice (with deep guards) of concurrent logic languages. A precise formal description requires the introduction of an existential quantifier for local variables and the distinction between global and local variables in the operational semantics. This is not included in this version but will be added in a

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
                          {l2=(e:r)} -> e:merge l1 r

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.

To encapsulate a possible non-deterministic search in a condition, one can simply replace the condition by a corresponding dummy choice. This has the effect that only one solution for the condition is taken into account. For instance, consider the following definition of a function f and a predicate p:

     f x | p x = x
     p a = True
     p b = True

The evaluation of the expression f x yields the disjunctive expression {x=a} a | {x=b} b since the evaluation of p x produces different bindings for the free variable x. If we replace the definition of f by

     f x | choice p x -> True  = x

then the same expression is reduced to {x=a} a or {x=b} b, where the chosen alternative depends on the implementation. Thus, an evaluation of f will never produce a disjunction with more than one alternative but not all possible answers are computed if it is called with a free variable argument.

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.

future version.

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].

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 data type 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)

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). This default strategy can be overridden by providing explicit evaluation annotations for each function or by the following pragmas which changes the default strategy for the remaining part of the module where they occur:

     default p

If p = narrow, then all arguments of all functions are flexible. If p = residuate, then all arguments of all functions (including the Booleans ones) are rigid. If p = standard, then it is switched backed to the standard strategy as described above. 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, 20] and Appendix D.5 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 1: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]} Valid | {L=[0],M=[1]} Valid | {L=[0,1],M=[]} Valid
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]} Valid

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 1:rigid
True  && x        = x
False && x        = False

-- Negation
not               :: Bool -> Bool
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 f []          = []
map f (x:xs)      = f x : map f xs
-- Accumulate all list elements
foldr             :: (a->b->b) -> b -> [a] -> b
foldr f z []      = z
foldr f z (x:xs)  = f x (foldr f z xs)
-- Filter elements in a list
filter            :: (A -> bool) -> list(A) -> list(A).
filter p []       = []
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

-- 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)

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.

• Both data and infix operator declarations are generalized

• 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: TypeConstrID, DataConstrID, TypeVarID, InfixOpID, FunctionID, VariableID. All, except Infix-OpID, 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. InfixOpID is any string of characters from the

string “~!@#$%^&*+-=<>?./|”.

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

Block ::= { [FixityDeclaration_{1} ; … FixityDeclaration_{n} [;]] n ⩾ 0

BlockDeclaration_{1} ; … BlockDeclaration_{m} [;] } m ⩾ 0

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 ::= TypeConstrID 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 ::= Position : FlexRigid

| rule

| Annotation or Annotation | Annotation and Annotation

Position ::= Natural

| Natural . Position

FlexRigid ::= FlexRigidKeyword [( ConsAnnot_{1} … ConsAnnot_{n} )] n > 0 FlexRigidKeyword ::= flex | rigid

ConsAnnot ::= ConstrID => Annotation

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

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

| DataConstrID

| ()

| ( ConstrTerm_{1} , … ConstrTerm_{n} ) n > 1 | ( DataConstID 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

PatternDeclaration ::= ConstrTerm = Expr [where LocalDefs]

CondExpr ::= | Constraint = Expr [CondExpr]

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

Constraint ::= { BasicConstraint_{1} , … BasicConstraint_{n} } n ⩾ 0 BasicConstraint ::= Expr = Expr

ChoiceExpr ::= choice {ChoiceBranch_{1} ; … ChoiceBranch_{n} [;] } n ≥ 0 ChoiceBranch ::= Constraint -> Expr

FunctExpr ::= [FunctExpr] BasicExpr BasicExpr ::= VariableID

| ()

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

Bool ::= see lexicon Int ::= see lexicon

Char ::= see lexicon String ::= see lexicon Float ::= see lexicon

In CondExpr, it is also allowed to write in the condition a Boolean expression b instead of a constraint which 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^{8}

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 and higher-order functions is described in Sections D.3 and D.4. Finally, Section D.5 describes the automatic generation of evaluation annotations if they are omitted by the programmer.

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).^{9} 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), where id denotes the identity substitution. 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) to ensure confluence. 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.

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.^{10} 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 = π.

8This section is based on material published in [20].

9Since 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}.

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

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 π.

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

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′.^{12} In the following, we write pattern(T ) for the pattern of a definitional tree T , and DT for the set of all definitional trees.

It is always possible to construct a definitional tree without and nodes for each function (concrete algorithms are described in [3, 27] and in Section D.5). For instance, the definitional tree for the predicate leq defined in Section 3 on page 10 is:

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))))

The and nodes are included only if concurrent computations should be allowed. Usually, an and node occur only in the definitional tree of the predefined concurrent conjunction /\ which is defined by the single rule

     Valid /\ Valid = Valid

together with the definitional tree

and(branch(x_{1}/\x_{2}, 1, rigid, branch(Valid/\x_{2}, 2, rigid, rule(Valid /\ Valid = Valid))),

branch(x_{1}/\x_{2}, 2, rigid, branch(x_{1}/\Valid, 1, rigid, rule(Valid /\ Valid = Valid))))

The and node in this tree specifies that an expression of the form e_{1} ∧e_{2} is evaluated by an attempt to evaluate 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 (see below for the formal specification).

D.2 Computation Steps

We provide a precise definition of the operational semantics using the functions

\begin{matrix}cse : & T (C ∪ F, X) → & D ∪ \{⊥\} \\ cs : & T (C ∪ F, X) × DT → & D ∪ \{⊥\} \end{matrix}

The function cse performs a single computation step on an expression e. It computes a disjunction of answer expressions or the special constant ⊥ indicating that no computation step is possible in e. As shown in Figure 1, cse attempts to apply a reduction step to the leftmost outermost function symbol in e by the use of cs which is called with the appropriate subterm and the definitional tree for the leftmost outermost function symbol. cs is defined by a case distinction on the definitional tree. If it is a rule node, we apply this rule. If the definitional tree is an and node, we try to evaluate the first branch and, if this is not possible due to the suspension of all function calls, the second branch.^{13} An or node produces a disjunction. To ensure completeness, we have to suspend the entire disjunction if one disjunct suspends [20]. 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, we either suspend (if the branch is rigid) or instantiate the variable to the different constructors. The auxiliary function replace puts a possibly disjunctive expression into a subterm:

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

12To ensure completeness, we have to require that the sets of rules in the different subtrees of an and node are identical.

replace(e, p, d) = \{ \begin{matrix}\{σ_{1} σ_{1}(e)[e_{1}]_{p}, …, σ_{n} σ_{n}(e)[e_{n}]_{p}\} & if d = \{σ_{1} e_{1}, …, σ_{n} e_{n}\} \\ ⊥ & if d = ⊥ \end{matrix}

The overall computation strategy transforms disjunctive expressions. It takes a disjunct σ e not in solved form and computes cse(e). If cse(e) = ⊥, then the computation of this expression flounders and we cannot proceed (i.e., this expression is not solvable). If cse(e) is 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 [20].

D.3 Conditional Rules

Following the approach taken in Babel [31], 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

     (Valid ⇒ 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.

D.4 Higher-Order Features

Warren [43] 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 [21, 32, 37]), the operational Computation step for a single (unsolved) expression:

13For the sake of simplicity, we choose a simple sequential strategy for concurrent computations. However, it is also possible to provide a more sophisticated strategy with a fair selection of threads, e.g., as in Oz [40].

cse(x)  = ⊥  for all variables x
cse(f(e_{1}, …, e_{n})) = cs(f(e_{1}, …, e_{n}), T ) if T is a definitional tree for f with fresh variables

\begin{matrix}cse(c(e_{1}, …, e_{n})) \\ = \{ \begin{matrix}replace(c(e_{1}, …, e_{n}), k, cse(e_{k})) & if cse(e_{1}) = ⋯ = cse(e_{k−1}) = ⊥ ≠ cse(e_{k}) \\ ⊥ & if cse(e_{i}) = ⊥, i = 1, …, n \end{matrix} \end{matrix}

Computation step for an operation-rooted expression e:

cs(e, rule(l = r)) = {id σ(r)}  if σ is a substitution with σ(l) = e
cs(e, and(T_{1}, T_{2})) = \{ \begin{matrix}cs(e, T_{1}) & if cs(e, T_{1}) ≠ ⊥ \\ cs(e, T_{2}) & otherwise \end{matrix}
cs(e, or(T_{1}, T_{2})) = \{ \begin{matrix}cs(e, T_{1}) ∪ cs(e, T_{2}) & if cs(e, T_{1}) ≠ ⊥ ≠ cs(e, T_{2}) \\ ⊥ & otherwise \end{matrix}

cs(e, branch(π, p, r, T_{1}, …, T_{k}))

= \{ \begin{matrix}cs(e, T_{i}) & if e|_{p} = c(e_{1}, …, e_{n}) and pat(T_{i})|_{p} = c(x_{1}, …, x_{n}) \\ ∅ & if e|_{p} = c(⋯) and pat(T_{i})|_{p} ≠ c(⋯), i = 1, …, k \\ ⊥ & if e|_{p} = x and r = rigid \\ ⋃_{i=1}^{k}\{σ_{i} σ_{i}(e)\} & if e|_{p} = x, r = flex, and σ_{i} = \{x = pat(T_{i})|_{p}\} \\ replace(e, p, cse(e|_{p})) & if e|_{p} = f(e_{1}, …, e_{n}) \end{matrix}

Derivation step for a disjunctive expression:

{σ e} ∪ D → {σ_{1} ∘ σ e_{1}, …, σ_{n} ∘ σ e_{n}} ∪ D

if σ e is unsolved and cse(e) = {σ_{1} e_{1}, …, σ_{n} e_{n}}

Figure 1: Operational semantics of Curry

semantics specified in Figure 1 can be simply extended to cover Curry’s higher-order features by adding the following equations for cse (here we denote by the infix operator “@” the application of a function to an expression):

cse(x@e)  = ⊥
cse(φ(e_{1}, …, e_{m})@e) = φ(e_{1}, …, e_{m}, e) if φ has arity n and m < n

The first equation specifies that the function application is “rigid” in its first argument, i.e., it delays if the applied function is unknown instead of a non-deterministic search for the appropriate function. The second equation adds an argument to a partial application.

λ-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 cse 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.5 Generating Definitional Trees

Our 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, we present in the following 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 [42]. 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 3, page 10) 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 “narrow” and “residuate”, see Section 9).

It is easy to see that this algorithm computes a definitional tree (without and nodes) 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 is conform with the evaluation strategy of functional languages like Haskell or Miranda, since it generates for the rules

     f 0 0 = 0
     f x 1 = 0

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 [42], then gt and optmatch generate identical definitional trees.

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). Springer LNCS (to appear), 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). MIT Press (to appear), 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. 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.

[21] 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.

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

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

[24] 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.

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

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

[27] 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.

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

[29] 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.

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

[31] 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.

[32] 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.

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

[34] 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.

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

[36] 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.

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

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

[39] 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.

[40] 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.

[41] 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.

[42] 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.

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

Index

(), 14 (...) (tuple type), 14 --, 30 ->, 12 /\, 7, 12, 35 :, 13 =, 4, 6

==, 6

>>, 15

>>=, 15

[], 13

[a] (list type), 13 &&, 11

{-...-}, 30

{...}, 7

annotation flexible, 10 rigid, 10

answer expression, 8, 34 application operator, 37 arity, 4

Bool, 11
Char, 14
choice, 16

comments, 30 computation step, 9 condition, 4 conditional equation, 4 conditional rule, 4 confluence, 5 conjunction, 7, 11, 12

concurrent, 7, 12, 35 of constraints, 7 sequential, 11

constant, 4

Constraint, 12

constraint, 6, 12

equational, 6 constructor, 3, 34 data term, 4, 34 ground, 4

data type declaration, 3

declaration data type, 3 function, 4 local, 5

                                            default, 19

defined function, 3, 34 defining equation, 4 definitional tree, 34 disjunctive expression, 9, 34

equality strict, 6 test, 6 equation, 4

conditional, 4 equational constraint, 6 evaluation annotation, 10, 32 expression, 4, 34 answer, 8, 34 disjunctive, 9, 34 ground, 4

                                            external, 18

external function, 18 extra variables, 5

                                            False, 11

flexible, 10

                                            Float, 13

function arity, 4 defined, 3, 34 external, 18 non-deterministic, 5 function application, 8, 37 function declaration, 4 function rule, 4

                                            getChar, 15
                                            getLine, 15

ground expression, 4 ground term, 4

head normal form, 10

Int, 12

IO, 15

λ-abstraction, 8, 37 left-hand side, 4 local declaration, 5

monadic I/O, 15

narrow, 19, 39

narrowing, 3, 9 non-deterministic function, 5

operation, 3, 34

optmatch, 19, 39

pattern, 34 position, 34 predicates, 11

putChar, 15
putStr, 15
putStrLn, 15
residuate, 19, 39

residuation, 3, 9

return, 15

right-hand side, 4 rigid, 10 root (of an expression), 34 rule, 4

conditional, 4

solved expression, 34

standard, 19

strict equality, 6

String, 14

subexpression, 34 substitution, 5, 34 subterm, 34

True, 11

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

unit type, 14

                                            Valid, 7

variable, 34 variant, 34

                                            where, 5