Curry

An Integrated Functional Logic Language

Draft of January 6, 1997

Michael Hanus^{1} [editor]

Additional Contributor:

Herbert Kuchen^{2}

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

Contents

1 Introduction 2

2 Programs 2 2.1 Data Type Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Function Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.3 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.4 Higher-order Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 Operational Semantics 6

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

5 Modules 11

6 Input/Output 11

7 Choice and Encapsulated Search 13

8 Interface to External Functions and Constraint Solvers 14 8.1 External Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 8.2 External Constraint Solvers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

9 Pragmas 15

10 Interactive Programming Environment 16

A Example Programs 17 A.1 Operations on Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 A.2 Higher-Order Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 A.3 Relational Programming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 A.4 Constraint Solving and Concurrent Programming . . . . . . . . . . . . . . . . . . . . 20

B Syntax of Curry 22

C Operational Semantics of Curry^{7} 23 C.1 Definitional Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 C.2 Computation Steps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 C.3 Conditional Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 C.4 Higher-Order Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 C.5 Generating Definitional Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

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 [16] 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 [20], SML [25]) 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 [19], λProlog [27]). Therefore, Curry is a strongly typed language with a Hindley/Milner-like polymorphic type system [9].^{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, List, 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 extension.

     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. A defining equation (or rule) for an n-ary function f has the form

f t_{1} … t_{n} | c = e where t_{1}, …, t_{n} are data terms and e is an expression. The condition “|c” (which can also be omitted) is an expression of type Bool. In order to apply this equation, its condition must be reduced to True.

To ensure that functions are well defined by a set of equations, a valid Curry program must satisfy the following restrictions:

1. For each rule f t_{1} … t_{n} | c = e, the left-hand side f t_{1} … t_{n} does not contain multiple occurrences of a variable, and each variable occurring in the right-hand side e must also occur in the 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 must hold:

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

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

These conditions ensure the confluence of the rules if they are considered as a conditional term rewriting system [36]. Note that we do not require the termination of the rewrite system so that the computation with infinite data structures is supported as in lazy functional languages. In contrast to functional languages, extra variables in the conditions (i.e., variables which do not occur in the left-hand side) are allowed. These extra variables provide the power of logic programming since a search for appropriate values is necessary in order to apply a conditional rule with extra variables.

Note that defining equations of higher-type, e.g., f = g if f and g are of type Bool -> Bool, are excluded by this definition since this would cause a gap between the standard notion of higherorder rewriting and the corresponding equational theory [30]. 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 Equality

A condition of a rule is a Boolean expression, which is also called a goal. To construct goals, Curry offers only a small number of primitives since the usual Boolean connectives can be defined as ordinary functions in Curry. For instance, the negation can be defined in Curry by

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

However, one exception is the equality, which needs particular attention. In the presence of nonterminating functions, the standard equality in the mathematical sense (congruence relation) is not reasonable [12, 26]. The only sensible notion of equality, which is also used in functional languages, is the strict equality l ≡ r that is satisfied if both sides l and r are reducible to a same ground data term. The strict equality could be explicitly defined by 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

     True ∧ x  =  x

This explicit definition has two disadvantages:

1. An equation x ≡ y between free variables is solved by binding x and y to all identical ground data terms, which is usually an infinite set.

2. The value False is not computed. This could be done by adding additional rules like

          c· · · ≡ d· · · = False

for all different constructors c and d, but this increases the number of different results computed in the first case.

To overcome this problem, Curry supports two kind of equalities which have an identical meaning on ground expressions but behave differently in the presence of free variables. The strict equality t_{1}==t_{2} tests whether t_{1} and t_{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 t_{1} and t_{2} is a free variable, t_{1}==t_{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

The second kind of strict equality, denoted t_{1}===t_{2}, requires that t_{1} and t_{2} must be equal in order to proceed the computation. This has the effect that t_{1} and t_{2} are evaluated to data terms which are finally unified. In particular, the equality x===y is solved by binding the variable x to y (or vice versa) instead of delaying the equation as for x==y. If the unification succeeds, the value True is computed, otherwise no value is computed, i.e., === is a partial function (see [13, 14, 24] for a more details on this subject). In terms of concurrent constraint programming languages [33], == and === correspond to ask and tell equality constraints, respectively.

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 goal 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 [18, 27, 32]. Since higher-order unification is a computationally expensive operation, Curry delays the application of unknown functions until the function becomes known [2, 35]. 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}}, also written as σ_{1} e_{1}| ⋯ |σ_{n} e_{n}.

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 defining a simple predicate:

     p a = True
     p b = True

The result of evaluating the goal p a is True, whereas the goal p X is evaluated to the disjunctive expression

     {X=a} True | {X=b} True .

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 [22, 23], Le Fun [2], Life [1], NUE-Prolog [29], or Oz [35]).

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 [15], Babel [26], K-Leaf [12], LPG [6], or SLOG [11]).

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.^{3} 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 unary predicate p above. Note that the argument is demanded since there are constructors in the left-hand sides of the rules. If p has the evaluation annotation

     p eval 1:flex

(1 denotes the first argument), then the goal p X is evaluated by instantiating X to a or b and applying a reduction step in both cases. This yields the disjunctive expression

     {X=a} True | {X=b} True

However, if p has the evaluation annotation

     p eval 1:rigid

then the goal p 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 goal (/\ denotes the conjunction of goals, see below):

     p X /\ X===b

Here, the first subterm p X cannot be evaluated and thus suspends, but the second subterm X===b is evaluated by binding X to b. After this binding, the first subterm can be evaluated and the entire goal is reduced to True:

     p X /\ X===b
     ⇝ {X=b} p b /\ True
     ⇝ {X=b} True /\ True
     ⇝ {X=b} True

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
     function 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).^{4} This dependency between the first and the second argument can be expressed by the evaluation annotation

3Evaluation annotations are similar to coroutining declarations [28] 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).

Since function calls may be suspended, we need a mechanism to specify concurrent computations. For this purpose, Curry provides a particular annotation to specify potentially concurrent evaluations. For instance, the (concurrent) conjunction /\ is defined by the single rule

     True /\ True = True

together with the evaluation annotation

     (/\) eval 1:rigid(True=>2:rigid) and 2:rigid(True=>1:rigid)

An and annotation can be used when more than one argument must be evaluated to apply some rule. Since all these arguments need to be evaluated to compute a result, it is also reasonable to evaluate these concurrently. This is exactly the meaning of the and annotation. An and annotation specifies a potentially concurrent computation of two arguments, i.e., the computation steps of the first and second argument can be interleaved. Thus, to evaluate the expression t_{1}/\t_{2}, we can evaluate t_{2} if the evaluation of the t_{1} suspends, or vice versa.

The general form of evaluation annotations is defined by the following grammar:

evalannot ::= funcid eval annotation % evaluation annotation
annotation ::= position : flexrigid  % evaluate position
| rule  % apply a rule
| annotation or annotation % alternative argument evaluations
| annotation and annotation % concurrent argument evaluations
position  ::= number  % positions in a function call
| number.position
flexrigid ::= rigid [ (consannot^{∗}) ]  % suspend if free variable
| flex [ (consannot^{∗}) ]  % instantiate free variable
consannot ::= cons => annotation  % cons is a constructor

Not all evaluation annotations generated by this grammar 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 C and form the basis of the operational semantics of Curry.

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

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

A precise specification of the operational semantics based on the evaluation annotations can be found in Appendix C.

4 Types

4.1 Built-in Types

The following types are predefined in Curry:

Boolean values: They are defined by the data type declaration

          data Bool = True | False

The conjunction of two goals, where both goals may be evaluated concurrently, is predefined as a left-associative infix operator

          (/\) :: Bool -> Bool -> Bool
          (/\) eval 1:rigid and 2:rigid
          True /\ True = True

(cf. Section 3 for the semantics of the eval annotation).

The sequential conjunction, which ignores its second argument if the first argument is False, is predefined as the left-associative infix operator &&:

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

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 goal x*x===y /\ x+x===y /\ digit x 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} True | {x=2,y=4} True

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:

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

denotes the list a_{1}:a_{2}:⋯:a_{n}:[] (which is equivalent to a_{1}:(a_{2}:(⋯:(a_{n}:[])...)) since “:” is a right-associative infix operator). The following functions define the concatenation of two lists and the application of a function to all elements in a list:

     append :: [a] -> [a] -> [a]
     append []     ys = ys
     append (x:xs) ys = x:append 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 [9]. 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 extension.

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 [15] or Gödel’s [19]. The extension to a more sophisticated module system like in SML [25] 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 [31] 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 doing I/O 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 ()
     putLine :: String -> IO ()

take a character (string) and produces an action which, when applied to a world, puts this character (string) to the standard output.

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 >>= \s->putLine s

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 goal which has the effect that the entire goal is split into two independent disjunctions. In order to avoid the splitting of the entire goal and to enable a “don’t care” selection of one element in a disjunction, Curry provides a primitive choice operation of the following form:^{5}

     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 Boolean expressions. This expression reduces to some e_{i} where the corresponding condition is provable, i.e., if, for some i ∈ {1, …, n}, c_{i} is reducible to ⋯| σ True |⋯, then the entire choice expression reduces to the single answer expression σ σ(e_{i}).^{6} 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 [13]. However, the completeness result for Curry’s operational semantics [17] 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.

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

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

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

Due to the use of the test equality == in the conditions, merge can also merge partially unknown list as long as the first elements of the lists are known.

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 goal is reduced to {x=a} a or {x=b} b, where the chosen alternative depends on the implementation. Thus, f is a well-defined deterministic function 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.

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 [7, 8].

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, 17] and Appendix C.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

Goals and their evaluated results:

append [0,1] [2,3] ⇝ [0,1,2,3]
append L M === [0,1]
   ⇝ {L=[],M=[0,1]} True | {L=[0],M=[1]} True | {L=[0,1],M=[]} True
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:
map :: (t1->t2) -> [t1] -> [t2]
map f []     = []
map f (x:xs) = f x:map f xs
% Fold a list:
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:
filter :: (t -> Bool) -> [t] -> [t]
filter p []     = []
filter p (x:xs) = ite (p x) (x:filter p xs) (filter p xs)
% if-then-else:
ite :: Bool -> a -> a -> a
ite True  x y = x
ite False x y = y
% Quicksort function:
quicksort :: [Int] -> [Int]
quicksort []      = []
quicksort (x:xs)  = append (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

Goals 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 negate the equality “==” by the following functions:

not :: Bool -> Bool
not True  = False
not False = True
diff :: a -> a -> Bool
diff x y = not (x==y)

For instance, diff t_{1} t_{2} has the value True if t_{1} and t_{2} are different constants. If one of the arguments is a variable, the evaluation of the function is delayed.

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 -> Bool
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 /\ 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

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

     diff l1 l2 /\ diff l1 l3 /\ diff l2 l3 /\ diff l2 l4 /\ diff l3 l4

which is then reduced to

     not (l1==l2) /\ not (l1==l3) /\ not (l2==l3) /\ not (l2==l4) /\ not (l3==l4)

This goal cannot be further evaluated since the arguments to == are free variables. Therefore, it is delayed and the final subexpression coloring l1 l2 l3 l4 is evaluated which binds the variables to the potential colors. Since the variable binding is performed by consecutive computation steps, the equality goals 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 subexpression not (l1==l2) is reduced to False which causes the failure of the entire goal. As a consequence, not all potential colorings are computed (as in the generate-and-test approach) but only those colorings for which the goal correct l1 l2 l3 l4 causes no failure. Therefore, the (dis)equality goals act as “passive constraints” aiming to reduce the search space.

B Syntax of Curry

To do: Provide a grammar for Curry

C Operational Semantics of Curry^{7}

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 C.1) which is the basis to define the computation steps on expressions (Section C.2). The extension of this basic computation model to conditional rules and higher-order functions is described in Sections C.3 and C.4. Finally, Section C.5 describes the automatic generation of evaluation annotations if they are omitted by the programmer.

C.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 [10] and functional logic programming [16].

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).^{8} 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 [10] 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.^{9} 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 = π.

7This section is based on material published in [17].

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

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

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′.^{11} 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, 24] and in Section C.5). The and nodes are included only if concurrent computations should be allowed. For instance, the definitional tree for the predicate leq defined in Section 3 on page 7 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))))

C.2 Computation Steps

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

cs : T (C ∪ F, X) → D ∪ {suspend}

and

cst : T (C ∪ F, X) × DT → D ∪ {suspend} .

The function cs performs a single computation step on an expression e. It computes a disjunction of answer expressions or the special constant suspend indicating that no reduction is possible in e. As shown in Figure 1, cs attempts to apply a reduction step to the leftmost outermost function symbol in e by the use of cst which is called with the appropriate subterm and the definitional tree for the leftmost outermost function symbol. cst 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.^{12} An or node produces a disjunction. To ensure completeness, we have to suspend the entire disjunction if one disjunct suspends [17]. For a similar reason, we cannot commit to a disjunct which does not bind variables but we have to consider both alternatives (see [5] 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 subterm. If it is a variable, we either suspend (if the branch is rigid) or instantiate the variable to the different constructors. The auxiliary function compose composes the result of a computation step with a substitution, and replace puts a possibly disjunctive expression into a subterm:

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

11To ensure completeness, we have to require that the sets of rules in the different subtrees of an and node are identical. Since we use and nodes only in conjunction with rigid branches in our examples, we can omit this requirement to simplify our examples.

12For 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 [35].

compose(e, T , σ) = \{ \begin{matrix}\{σ e\} & if cst(e, T ) = suspend \\ \{σ_{1} ∘ σ e_{1}, …, σ_{n} ∘ σ e_{n}\} & if cst(e, T ) = \{σ_{1} e_{1}, …, σ_{n} e_{n}\} \end{matrix}

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

The overall computation strategy is a transformation ⟶^{RN} on disjunctive expressions. It takes a disjunct σ e not in solved form and computes cs(e). If cs(e) = suspend, then the computation of this expression flounders and we cannot proceed (i.e., this expression is not solvable). If cs(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 [17].

C.3 Conditional Rules

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

     (True ⇒ x)  =  x .

Thus, a guarded expression is evaluated by an attempt to reduce the condition to True. If the condition c is evaluable to True, the guarded expression c ⇒ r is replaced by r, i.e., by the righthand side of the conditional rule. If the condition is not evaluable to True and does not suspend, the disjunct containing this guarded expression will be deleted by definition of ⟶^{RN}, i.e., the application of the conditional rule fails and does not contribute to the final result.

C.4 Higher-Order Features

Warren [38] has shown 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 [18, 27, 32]), the operational semantics specified in Figure 1 can be simply extended to cover Curry’s higher-order features by adding the following equations for cs (here we denote by the infix operator “@” the application of a function to an expression):

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

Computation step for a single (unsolved) expression:

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

\begin{matrix}cs(c(e_{1}, …, e_{n})) \\ = \{ \begin{matrix}replace(c(e_{1}, …, e_{n}), k, cs(e_{k})) & if cs(e_{i}) = suspend, i = 1, …, k − 1, and cs(e_{k}) ≠ suspend \\ suspend & if cs(e_{i}) = suspend, i = 1, …, n \end{matrix} \end{matrix}

Computation step for an operation-rooted expression e:

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

cst(e, branch(π, o, r, T_{1}, …, T_{k}))

= \{ \begin{matrix}cst(e, T_{i}) & if e|_{o} = c(e_{1}, …, e_{n}) and pattern(T_{i})|_{o} = c(x_{1}, …, x_{n}) \\ ∅ & if e|_{o} = c(e_{1}, …, e_{n}) and pattern(T_{i})|_{o} ≠ c(⋯), i = 1, …, k \\ suspend & if e|_{o} = x and r = rigid \\ ⋃_{i=1}^{k} compose(σ_{i}(e), T_{i}, σ_{i}) & if e|_{o} = x, r = flex, and σ_{i} = \{x ↦ pattern(T_{i})|_{o}\} \\ replace(e, o, cs(t|_{o})) & if e|_{o} = f(e_{1}, …, e_{n}) \end{matrix}

Derivation step for a disjunctive expression:

{σ e} ∪ D ⟶^{RN} {σ_{1} ∘ σ e_{1}, …, σ_{n} ∘ σ e_{n}} ∪ D

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

Figure 1: Operational semantics of Curry

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

C.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 [37]. 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 7) 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 [13] or conditional rules are transformed into unconditional rules (see Section C.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 [37], 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, R. Echahed, and M. Hanus. A Needed Narrowing Strategy. In Proc. 21st ACM Symposium on Principles of Programming Languages, pp. 268–279, Portland, 1994.

[5] S. Antoy, R. Echahed, and M. Hanus. A Parallel Narrowing Strategy. Technical Report TR 96-1, Portland State University, 1996.

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

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

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

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

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

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

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

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

[14] J.C. González-Moreno, M.T. Hortalá-González, and M. Rodríguez-Artalejo. On the Completeness of Narrowing as the Operational Semantics of Functional Logic Programming. In Proc. CSL’92, pp. 216–230. Springer LNCS 702, 1992.

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

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

[17] M. Hanus. A Unified Computation Model for Functional and Logic Programming. In Proc. of the 24th ACM Symposium on Principles of Programming Languages (to appear), 1997.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Index

(), 11 (...) (tuple type), 11

->, 9

/\, 8, 9 :, 10 =, 3

==, 4
===, 5

>>, 12

>>=, 12

[], 10

[a] (list type), 10

&&, 9

annotation flexible, 7 rigid, 7

answer expression, 6, 23 application operator, 25 arity, 3

Bool, 9
Char, 10
choice, 13

computation step, 6 condition, 3 confluence, 4 conjunction, 8, 9

concurrent, 8, 9 sequential, 9

constant, 3 constructor, 2, 23

data term, 3, 23 data type declaration, 2 declaration

data type, 2 function, 3

default, 15

defined function, 2, 23 defining equation, 3 definitional tree, 23 disjunctive expression, 6, 23

equality strict, 4 tell, 5 test, 4 equation, 3 evaluation annotation, 7, 8 expression, 3, 23 answer, 6, 23 disjunctive, 6, 23

                                            external, 14

external function, 14 extra variables, 4

                                            False, 9

flexible, 7

                                            Float, 10

function arity, 3 defined, 2, 23 external, 14

function application, 5, 25 function declaration, 3 function rule, 3

                                            getChar, 12
                                            getLine, 12

goal, 4

ground expression, 3

ground term, 3

head normal form, 7

                                            Int, 10

IO, 12

λ-abstraction, 5, 26 left-hand side, 3

monadic I/O, 12

                                            narrow, 15, 28

narrowing, 2, 6 operation, 2, 23

optmatch, 15, 28

pattern, 23 position, 8, 23 predicates, 9

putChar, 12
putLine, 12
residuate, 15, 28

residuation, 2, 6

return, 12

right-hand side, 3 rigid, 7 root (of an expression), 23 rule, 3

solved expression, 23

standard, 15

strict equality, 4

String, 11

subexpression, 23 substitution, 3, 23 subterm, 23

True, 9

tuple, 11 type constructor, 2 type declaration, 2, 3 type expression, 2 type variable, 2

unit type, 11

variable, 23 variant, 23