Basic Features of Curry

Values in Curry are, similarly to functional or logic languages, data terms constructed from constants and data constructors. For instance, the datatype declarations

data Bool = True | False

data List a = [] | a : List a

introduce the datatype  $$Bool  with the 0-ary constructors (constants)  $$True  and  $$False, and the polymorphic type  $$List a  of lists similar to functional languages. Natural numbers, which we will use in the examples, are represented in Curry by constants of type  $$Int.

A data term is a well-typed expression containing variables, constants and data constructors, e.g.,  $$1:2:x. Functions operate on data terms. Their meaning is specified by rules (or equations) of the form  $$l |c = r  (the condition part `` $$|c '' is optional) where $l$ is a pattern, i.e., $l$ has the form $f\; t$₁...t_n with $f$ being a function, $t$₁,...,t_n data terms and each variable occurs only once, and $r$ is a well-formed expression containing function calls, constants, data constructors and variables from $l$ and $c$. The condition $c$ is usually a constraint which consists of a conjunction of equations and optionally contains a list of locally declared variables, i.e., a constraint can have the form  $$let  $v$₁,...,v_k  $$free in  $eq$₁&...&eq_n where the variables $v$_i are only visible in the equations $eq$₁,...,eq_n. If a local variable $v$ of a condition should be visible also in the right-hand side, the rule is written as  $$l |c = r  where v free. A rule can be applied if its condition is satisfiable. A head normal form is a variable, a constant, or an expression of the form $c\; e$₁...e_n where $c$ is a data constructor. A Curry program is a set of data type declarations and equations.

 

From a functional point of view, we are interested in computing the value of an expression, i.e., a data term which is equivalent (w.r.t. the program rules) to the initial expression. In contrast, we want to solve goals like in logic languages, i.e., compute bindings for free variables in an initial expression, if we concentrate on the logic part of Curry. Since the language integrates the two paradigms, it computes answer pairs consisting of a substitution and an expression. Due to the nondeterministic features of Curry, an expression may reduce to more than one answer pair, i.e., a reduction step has the general form

where , $e$, $e$₁,...,$e$_n are expressions, are substitutions on the free variables in $e$, and `` $$| '' joins different alternatives to a disjunction. We call the evaluation step deterministic if n$=$1 and nondeterministic if n$>$1. The case n$=$0 corresponds to a failure.

For selecting the next reducible function call in an expression that must be evaluated, Curry uses a combination of residuation and needed narrowing  [1, 8]. This is, roughly speaking, the combination of lazy evaluation with bindings of uninstantiated variables as demanded by the patterns of left-hand sides in the rules. For instance, consider the function  $$sq  from Example 1. The function call  $$sq 2  is reduced to the value  $$4  like in any functional language. But if we pass an uninstantiated variable as argument, there are two possibilities:

1. If we evaluate  $$sq  by residuation, the call  $$sq x  will suspend until  $$x  is bound to some constructor term that will allow to choose one of the rules for reduction. This can be achieved for instance by concurrent evaluation of constraints where a different thread can bind  $$x  to some value. Then the evaluation of the call to  $$sq  will be continued. We will not sketch this mechanism further because it is not the interesting case for our analysis.
2. If we evaluate  $$sq  by narrowing (as it will be done in all following examples), then we bind  $$x  to all possible patterns of the left-hand sides and continue with all different computation branches independently:

   

   Thus, the call  $$sq x  causes a nondeterministic step in our computation.

In Curry, constraints are evaluated by narrowing, because they correspond to goals in logic languages, while non-constraint functions are computed using residuation. This behavior can be changed by annotations [12]. In the following we will use  $$case -expressions for functions which are more feasible for our analysis because they provide for a consistent form of the rules (only variables as arguments in the left-hand side and only one right-hand side) and encode pattern matching explicitly. Additionally, they enable us to transfer the information about the reduction method into the function definition. Thus, the  $$sq  function can be rewritten as

sq x = case x of 1:1;2:4

if it should be evaluated by residuation, and as

sq x = fcase x of 1:1;2:4

to use narrowing for its evaluation (a precise definition of this transformation can be found in [9]).

Additionally to narrowing, nondeterminism in Curry can also be caused by nondeterministic functions, i.e., functions with overlapping left-hand sides in their rules. For instance, the following nondeterministic 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 nondeterministic functions can be given a perfect declarative semantics [6] and their evaluation causes no problems in Curry due to the already present nondeterministic evaluation principle. For instance, the expression  $$insert 1 (0:2:[])  will after one step return a disjunction of two answer pairs just like a nondeterministic step caused by narrowing would do. For our analysis we will use  $$or -expressions to encode this form of nondeterminism. Thus, the  $$insert  function would be written as:

insert x z = case z of []    :[x];

                       (y:ys):or(x : y : ys,

                                 y : insert x ys)

Nesting the binary  $$or  operator allows to encode functions with more than two overlapping left-hand sides.

Note that after transforming a program into case- and or-expressions, every rule has a left-hand side of the form $f\; x$₁... x_n where the $x$_i are variables.