programs.tex

\section{Programs}
\label{sec-programs}

A Curry program specifies the semantics of expressions.
Executing a Curry program means simplifying an expression until
a value (together with bindings of free variables) is computed.
To distinguish between values and reducible expressions,
Curry has a strict distinction between (data)
\emph{constructors}\index{constructor} and
\emph{operations}\index{operation} or
\emph{defined functions}\index{defined function}\index{function!defined}
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\index{predicate} in the logic programming sense can be considered
as functions with result type \code{Bool}.
Goals, which are the main expressions in logic programming,
are Boolean expressions that are intended to be evaluated to \code{True}.

Modern functional languages (e.g., Haskell \cite{PeytonJones03Haskell},
SML \cite{MilnerTofteHarper90}) 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\"odel \cite{HillLloyd94}, $\lambda$Prolog \cite{NadathurMiller88}).
Curry follows the same approach, i.e., it is a strongly typed language with a
Hindley/Milner-like polymorphic type system \cite{DamasMilner82}.\footnote{%
The extension of this type system to Haskell's type classes
is not included in the kernel language but could be considered
in a future version.}
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.


\subsection{Datatype Declarations}
\label{sec-datatypes}

A datatype declaration\index{type declaration}\index{datatype!declaration}
\index{declaration!datatype} has the form
\begin{curry}
data $T$ $\alpha_1\ldots{}\alpha_n$ = $C_1$ $\tau_{11}\ldots{}\tau_{1n_1}$ | $\cdots$ | $C_k$ $\tau_{k1}\ldots{}\tau_{kn_k}$
\end{curry}
and introduces a new $n$-ary \emph{type constructor}\index{type constructor}
$T$ and $k$
new (data) \emph{constructors} $C_1,\ldots,C_k$, where each $C_i$ has the type
\begin{curry}
$\tau_{i1}$ -> $\cdots$ -> $\tau_{in_i}$ -> $T~\alpha_1\ldots\alpha_n$
\end{curry}
($i=1,\ldots,k$). Each $\tau_{ij}$ is a
\emph{type expression}\index{type expression} built from the
\emph{type variables}\index{type variable} $\alpha_1,\ldots,\alpha_n$
and some type constructors. Curry has a number of built-in type constructors,
like \code{Bool}, \code{Int}, \code{->} (function space), or, lists and tuples,
which are described in Section~\ref{sec-builtin-types}.
Since Curry is a higher-order language,
the types of functions (i.e., constructors or operations)
are written in their curried form
\code{$\tau_1$ -> $\tau_2$ -> $\cdots$ -> $\tau_n$ -> $\tau$}
where $\tau$ is not a functional type.
In this case, $n$ is called the \emph{arity}\index{arity}\index{function!arity}
of the function.
For instance, the datatype declarations
\begin{curry}
data Bool = True | False
data List a = [] | a : List a
data Tree a = Leaf a | Node (Tree a) a (Tree a)
\end{curry}
introduces the datatype \code{Bool} with the 0-ary constructors
(\emph{constants})\index{constant} \code{True} and \code{False},
and the polymorphic types \code{List a} and \code{Tree a} of lists
and binary trees. Here, \ccode{:} is an infix operator, i.e.,
``\code{a:List a}'' is another notation for ``\code{(:) a (List a)}''.
Lists are predefined in Curry, where the notation ``\code{[a]}''
is used to denote list types (instead of ``\code{List a}'').
The usual convenient notations for lists are supported,
i.e., \code{[0,1,2]} is an abbreviation for
\code{0:(1:(2:[]))} (see also Section~\ref{sec-builtin-types}).

A \emph{data term}\index{data term} is a variable $x$ or a
constructor application
$c~t_1\ldots t_n$ where $c$ is an $n$-ary constructor and
$t_1,\ldots,t_n$ are data terms. An \emph{expression}\index{expression}
is a variable or a (partial) application $\varphi~e_1 \ldots e_m$
where $\varphi$ is a function or constructor
and $e_1,\ldots,e_m$ are expressions.
A data term or expression is called \emph{ground}\index{ground expression}
\index{expression!ground}\index{ground term}\index{data term!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.


\subsection{Type Synonym Declarations}
\label{sec-typesyns}

To make type definitions more readable, it is possible
to specify new names for type expressions by a
\emph{type synonym declaration}.\index{type synonym declaration}
\index{type!synonym declaration}\index{declaration!type synonym}
Such a declaration has the general form
\begin{curry}
type $T$ $\alpha_1\ldots{}\alpha_n$ = $\tau$
\end{curry}
which introduces a new $n$-ary type constructor\index{type constructor}
$T$. $\alpha_1,\ldots,\alpha_n$ are pairwise distinct type variables
and $\tau$ is a type expressions built from type constructors
and the type variables $\alpha_1,\ldots,\alpha_n$.
The type \code{($T$ $\tau_1\ldots \tau_n$)} is equivalent to the
type $\{\alpha_1 \mapsto \tau_1,\ldots,\alpha_n\mapsto\tau_n\}(\tau)$,
i.e., the type expression $\tau$ where each $\alpha_i$ is replaced
by $\tau_i$. Thus, a type synonym and its definition
are always interchangeable and have no influence on the
typing of a program. For example, we can provide an alternative
notation for list types and strings by the following
type synonym declarations:
\begin{curry}
type List a = [a]
type Name = [Char]
\end{curry}
Since a type synonym introduces just another name for a type
expression, recursive or mutually dependent type synonym declarations
are not allowed. Therefore, the following declarations are \emph{invalid}:
\begin{curry}
type RecF a = a -> RecF a   -- recursive definitions not allowed
type Place = [Addr]         -- mutually recursive definitions not allowed
type Addr = [Place]
\end{curry}
However, recursive definitions with an intervening datatype are allowed,
since recursive datatype definitions are also allowed.
For instance, the following definitions are valid:
\begin{curry}
type Place = [Addr]
data Addr = Tag [Place]
\end{curry}


\subsection{Function Declarations}
\label{sec-funcdecl}

A function is defined by a type declaration (which can be omitted)
followed by a list of defining equations.
%
A \emph{type declaration}\index{type declaration}\index{function declaration}
\index{declaration!function} has the form
\begin{curry}
$f$ :: $\tau_1$ -> $\tau_2$ -> $\cdots$ -> $\tau_k$ -> $\tau$
\end{curry}
where $\tau_1,\ldots,\tau_k,\tau$ are type expressions.

The simplest form of a
\emph{defining equation}\index{equation}\index{defining equation}
(or \emph{rule})\index{rule}\index{function rule}\pindex{=}
for an $n$-ary function $f$ ($n \geq 0$) is
\begin{curry}
$f~t_1\ldots t_n$ = $e$
\end{curry}
where $t_1,\ldots,t_n$ are data terms (also called \emph{patterns}\index{pattern})
and the \emph{right-hand side}\index{right-hand side} $e$ is an expression.
Functions can also be defined by
\emph{conditional equations}\index{conditional equation}%
\index{equation!conditional}\index{conditional rule}\index{rule!conditional}
which have the form
\begin{curry}
$f~t_1\ldots t_n$ | $c$ = $e$
\end{curry}
where the \emph{condition}\index{condition} $c$ is a Boolean expression
A conditional equation can be applied if its condition can be
evaluated to \code{True}.

If the \emph{left-hand side}\index{left-hand side}
$f~t_1\ldots t_n$ of a defining equation contains multiple occurrences
of a variable,\index{multiple variables in left-hand sides}
these occurrences are considered as an
equational constraint\index{equational constraint}
\index{constraint!equational} (cf.\ Section~\ref{sec-equality})
between the arguments. Thus, a function declaration
\begin{curry}
f x x = g x
\end{curry}
is considered as an abbreviation of the conditional equation
\begin{curry}
f x y | x=:=y = g x
\end{curry}
Thus, each multiple variable occurrence is replaced by a new
variable and an equational constraint is added.
These constraints are the first constraints to be solved.
For instance, the conditional equation
\begin{curry}
f x y x y | c x y = g x
\end{curry}
is considered as an abbreviation for
\begin{curry}
f x y x1 y1 | (x=:=x1 & y=:=y1) &> c x y = g x
\end{curry}
%
An $n$-ary function $f$ can be defined by more than one
(conditional) equation (where each rule must have the same number
of arguments on the left-hand side).
Note that one can define functions with a non-determinate
behavior by providing several rules with overlapping left-hand sides
or \emph{free variables}\index{free variable}\index{variable!free}
(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:\label{ex-insert}
\begin{curry}
insert x []     = [x]
insert x (y:ys) = x : y : ys
insert x (y:ys) = y : insert x ys
\end{curry}
Such \emph{non-deterministic functions}\index{non-deterministic function}
\index{function!non-deterministic}
can be given a perfect declarative semantics \cite{GonzalezEtAl99}
and their implementation causes no overhead in Curry
since techniques for handling non-determinism are already contained in
the logic programming part (see also \cite{Antoy97ALP}).
However, deterministic functions are advantageous since
they provide for more efficient implementations (like the
\emph{dynamic cut} \cite{LoogenWinkler95}).
If one is interested only in defining deterministic functions,
this can be ensured by the following restrictions:
\begin{enumerate}
\item
Each variable occurring in the right-hand side of a rule
must also occur in the corresponding left-hand side.
\item
If \code{~$f~t_1\ldots t_n$ | $c$ = $e$~} and
\code{~$f~t'_1\ldots t'_n$ | $c'$ = $e'$~} are rules defining $f$ and
$\sigma$ is a \emph{substitution}\index{substitution}\footnote{%
A \emph{substitution} $\sigma$ is a mapping from variables into expressions
which is extended to a homomorphism on expressions by defining
$\sigma(f~t_1\ldots t_n) = f~\sigma(t_1)\ldots \sigma(t_n)$.
$\{x_1 \mapsto e_1,\ldots,x_k \mapsto e_k\}$ denotes the substitution
$\sigma$ with $\sigma(x_i)=e_i$ ($i=1,\ldots,k$) and
$\sigma(x)=x$ for all variables $x\not\in\{x_1,\ldots,x_k\}$.}
with $\sigma(t_1\ldots t_n)=\sigma(t'_1\ldots t'_n)$, then at least
one of the following conditions holds:
\begin{enumerate}
\item $\sigma(e)=\sigma(e')$ (\emph{compatibility of right-hand sides}).
\item $\sigma(c)$ and $\sigma(c')$ are not simultaneously satisfiable
(\emph{incompatibility of conditions}). A decidable approximation
of this condition can be found in \cite{KuchenEtAl96NGC}.
\end{enumerate}
\end{enumerate}
These conditions ensure the confluence\index{confluence}
of the rules if they are considered as a conditional term rewriting
system \cite{SuzukiMiddeldorpIda95RTA}.
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 \cite{SuzukiMiddeldorpIda95RTA}
which can be checked instead of the above conditions.


\subsubsection{Functions vs.\ Variables}
\label{sec-variable-sharing}

In lazy functional languages, different occurrences of the same
variable are shared to avoid multiple evaluations of
identical expressions. For instance, if we apply the rule
\begin{curry}
double x = x+x
\end{curry}
to an expression \code{double$\,t$}, we obtain the new expression
\code{$t$+$t$} but both occurrences of $t$ denote the identical
expression, i.e., these subterms will be simultaneously evaluated.
Thus, \emph{several occurrences of the same variable are
always shared},\index{sharing}
i.e., if one occurrence of an argument variable,
which might bound to an evaluable expression when the function
is applied, is evaluated to some value, all other occurrences
of this variable are replaced by the same value (without
evaluating these other occurrences again).
This sharing is necessary not only for efficiency reasons
but it has also an influence on the soundness of the operational semantics
in the presence of non-deterministic functions
(see also \cite{GonzalezEtAl99}). For instance,
consider the non-deterministic function \code{coin} defined by the rules
\begin{curry}
coin = 0
coin = 1
\end{curry}
Thus, the expression \code{coin} evaluates to \code{0} or \code{1}.
However, the result values of the expression \code{(double\,\,coin)}
depend on the sharing of the two occurrences of \code{coin}
after applying the rule for \code{double}: if both occurrences
are shared (as in Curry), the results are \code{0} or \code{2},
otherwise (without sharing) the results are \code{0}, \code{1}, or \code{2}.
The sharing of argument variables corresponds to the so-called
``call time choice'' in the declarative semantics
\cite{GonzalezEtAl99}: if a rule is applied to a function call,
a unique value must be assigned to each argument
(in the example above: either \code{0} or \code{1} must be assigned
to the occurrence of \code{coin} when the expression
\code{(double\,\,coin)} is evaluated). This does not mean that
functions have to be evaluated in a strict manner but this
behavior can be easily obtained by sharing the different occurrences
of a variable.

Since different occurrences of the same variable are always shared
but different occurrences of (textually identical) function
calls are not shared, it is important to distinguish
between variables and functions. Usually, all symbols
occurring at the top level in the left-hand side of some rule
are considered as functions and the non-constructor symbols
in the arguments of the left-hand sides are considered
as variables. But note that there is a small exception
from this general rule in local declarations
(see Section~\ref{sec-localdecls}).


\subsubsection{Rules with Multiple Guards}
\label{sec-bool-guards}

One can also write conditional equations with multiple guards
\begin{curry}
$f~t_1\ldots t_n$ | $b_1$ = $e_1$
         $\,\vdots$
         | $b_k$ = $e_k$
\end{curry}
where $b_1,\ldots,b_k$ ($k>0$) are expressions of type \code{Bool}.
Such a rule is interpreted as in Haskell: the guards are successively evaluated
and the right-hand side of the first guard which is evaluated to \code{True}
is the result of applying this equation. Thus, this equation
can be considered as an abbreviation for the rule
\begin{curry}
$f~t_1\ldots t_n$ = if $b_1$ then $e_1$ else
           $\vdots$
           if $b_k$ then $e_k$ else failed
\end{curry}
(where \code{failed}\pindex{failed} is a non-reducible function
defined in the prelude).
To write rules with several Boolean guards more nicely,
there is a Boolean function \code{otherwise}\pindex{otherwise}
which is predefined as \code{True}. For instance, the factorial
function can be declared as follows:
\begin{curry}
fac n | n==0      = 1
      | otherwise = fac(n-1)*n
\end{curry}
After performing a simple optimization, this definition is equivalent to
\begin{curry}
fac n = if n==0 then 1 else fac(n-1)*n
\end{curry}
%
Note that multiple guards in a single rule are always sequentially tested,
whereas multiple rules for a function are non-deterministically applied
(see the definition of \code{insert} in in Section~\ref{ex-insert}).
Thus, the following definition of \code{fac} has a different
meaning than the definition with multiple guards above,
since the second rule is always applicable:
\begin{curry}
fac n | n==0      = 1
fac n | otherwise = fac(n-1)*n
\end{curry}


\subsubsection{As-Patterns}

The patterns in a defining equation, i.e., the arguments of the left-hand sides,
are required to be data terms without multiple occurrences of variables.
Patterns are useful to split the definition of functions into
easily comprehensible cases. Thus, a pattern denotes some
part of a structure of the actual argument. Sometimes one wants to
reuse this structure in the right-hand side of the defining equation.
This can be expressed by an \emph{as-pattern}\index{as-pattern}\pindex{"@}
which allows to identify this structure by a variable.
An as-pattern has the form \code{$v$@$pat$} where the variable $v$
identifies the structure matched by the pattern $pat$.
For instance,
\begin{curry}
dropFalse (False:ys)  = ys
dropFalse xs@(True:_) = xs
\end{curry}
is equivalent to
\begin{curry}
dropFalse0 xs = dropFalse' xs
 where
  dropFalse' (False:ys)  = ys
  dropFalse' (True:_)    = xs
\end{curry}
(local declarations introduced by \code{where}-clauses are discussed
in Section~\ref{sec-localdecls}). However, as-patterns are usually implemented
more efficiently without introducing an auxiliary function.


\subsection{Local Declarations}
\label{sec-localdecls}

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

An expression of the form \code{let {\it{}decls} in {\it{}exp}}
\index{local declaration}\index{declaration!local}\pindex{let}
introduces a set of local names. The list of local declarations
\emph{decls} can contain function definitions as well as
definitions of constants by pattern matching. The names
introduced in these declarations are visible in the expression
\emph{exp} and the right-hand sides of the declarations in \emph{decls},
i.e., the local declarations can be mutually recursive.
For instance, the expression
\begin{curry}
let a=3*b
    b=6
in 4*a
\end{curry}
reduces to the value \code{72}.

Auxiliary functions which are only introduced to define another
function should often not be visible outside. Therefore,
such functions can be declared in a \code{where}-clause
\index{local declaration}\index{declaration!local}\pindex{where}
added to the right-hand side of the corresponding function definition.
This is done in the following definition of a fast exponentiation
where the auxiliary functions \code{even} and \code{square}
are only visible in the right-hand side of the rule for \code{exp}:
\begin{curry}
exp b n = if n==0
          then 1
          else if even n then square (exp b (n `div` 2))
                         else b * (exp b (n-1))

       where even n = n `mod` 2 == 0
             square n = n*n
\end{curry}
Similarly to \code{let}, \code{where}-clauses can contain
mutually recursive function definitions as well as
definitions of constants by pattern matching.
The names declared in the \code{where}-clauses are only visible
in the corresponding conditions and right-hand sides.
As a further example, the following Curry program implements
the quicksort algorithm with a function \code{split} which
splits a list into two lists containing the smaller and larger elements:
\begin{curry}
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
\end{curry}
To distinguish between locally introduced functions and variables
(see also Section~\ref{sec-variable-sharing}),
we define a \emph{local pattern}\index{local pattern}\index{pattern!local}
as a (variable) identifier or an application where the top symbol
is a data constructor. If the left-hand side of a local declaration
in a \code{let} or \code{where} is a pattern, then all identifiers
in this pattern that are not data constructors are
considered as variables. For instance, the locally introduced
identifiers \code{a}, \code{b}, \code{l}, and \code{r} in the previous examples
are variables whereas the identifiers \code{even} and \code{square}
denote functions. Note that this rule exclude the
definition of 0-ary local functions since a definition of the form
``\code{where f = \ldots}'' is considered as the definition of
a local variable \code{f} by this rule which is usually the intended
interpretation (see previous examples).
Appendix~\ref{app-lifting} contains a precise formalization
of the meaning of local definitions.


\subsection{Free Variables}
\label{sec-freevars}

Since Curry is intended to cover functional as well as logic
programming paradigms, expressions might contain free
(unbound, uninstantiated) variables.
\index{variable!free}\index{free variable}\index{unbound variable}
The idea is to compute values
for these variables such that the expression is reducible
to a data term.
For instance, consider the definitions\label{ex-persons}
\begin{curry}
data Person = John | Christine | Alice | Andrew

mother John    = Christine
mother Alice   = Christine
mother Andrew  = Alice
\end{curry}
Then we can compute a child of \code{Alice} by solving the
equation (see Section~\ref{sec-equality})
\begin{curry}
mother x == Alice
\end{curry}
Here, \code{x} is a free variable
which is instantiated to \code{Andrew} in order to reduce
the equation's left-hand side to \code{Alice}
and compute the result \code{True} for this equation.
Note that we can also compute the result \code{False}
by instantiating \code{x} to \code{John} or \code{Alice}.
If we are interested to obtain only positive solutions,
we can wrap the initial expression with the operation
\code{solve}\pindex{solve}, which is defined in the prelude by
the single rule
\begin{curry}
solve True = True
\end{curry}
Hence, the equation
\begin{curry}
solve (mother x == Alice)
\end{curry}
reduces only to \code{True} and yields the value \code{Andrew} for \code{x}.
Using the infix application operator \code{\$} defined in the prelude,
we can omit the parentheses and write this equation as
\begin{currynomath}
solve $ mother x == Alice
\end{currynomath}% $
%
Similarly, we can compute a grandchild of \code{Chistine}
by solving the equation
\begin{curry}
mother (mother x) == Christine
\end{curry}
which yields the value \code{Andrew} for \code{x}.

In logic programming languages like Prolog, all free variables
are considered as existentially quantified at the top level.
Thus, they are always implicitly declared at the top level.
In a language with different nested scopes like Curry,
it is not clear to which scope an undeclared variable belongs
(the exact scope of a variable becomes particularly important
in the presence of search operators, see Section~\ref{sec-encapsearch},
where existential quantifiers and lambda abstractions are often
mixed). Therefore, Curry requires that
\emph{each free variable $x$ must be explicitly declared}
using a local declaration \index{declaration!free}\index{free declaration}
\index{variable!declaration}
of the form \code{$x$ free}.\pindex{free}
The variable is then introduced as unbound
with the same scoping rules as for all other local
entities (see Section~\ref{sec-localdecls}).
For instance, we can define
\begin{curry}
isGrandmother g | let c free in mother (mother c) == g  = True
\end{curry}
An exception are \emph{anonymous free variables}\index{variable!anonymous}%
\index{anonymous free variable}, i.e.,
free variables occurring only once in an expression,
which can be denoted by \ccode{\us}.
Thus, each occurrence of \ccode{\us} in an expression
can be considered as an abbreviation of \ccode{let x free in x}.

As a further example, consider the definition of the
concatentation of two lists:
\begin{curry}
append []     ys = ys
append (x:xs) ys = x : append xs ys
\end{curry}
Then we can define the function \code{last} which computes
the last element of a list by the rule
\begin{curry}
last zs | append xs [x] == zs  = x  where x,xs free
\end{curry}
Since the variable \code{xs} occurs in the condition but not in the
right-hand side, the following definition is also possible:
\begin{curry}
last zs | let xs free in append xs [x] == zs  = x  where x free
\end{curry}
which can abbreviated to
\begin{curry}
last zs | append _ [x] == zs  = x  where x free
\end{curry}
%
Note that the \code{free} declarations can be freely mixed with
other local declarations after a \code{let} or \code{where}.
The only difference is that a declaration like ``\code{let x free}''
introduces an unbound variable whereas
other \code{let} declarations introduce local functions or parameters.
Since all local declarations can be mutually recursive,
it is also possible to use local variables in the bodies
of the local functions in one \code{let} declarations.
For instance, the following expression is valid (where the functions
\code{h} and \code{k} are defined elsewhere):
\begin{curry}
let f x = h x y
    y free
    g z = k y z
 in c y (f (g 1))
\end{curry}
Similarly to the usual interpretation of local definitions
by lambda lifting \cite{Johnsson85}, this expression
can be interpreted by transforming the local definitions
for \code{f} and \code{g} into global ones by adding the non-local
variables of the bodies as parameters:
\begin{curry}
f y x = h x y
g y z = k y z
$\ldots$
  let y free in c y (f y (g y 1))
\end{curry}
See Appendix~\ref{app-lifting} for more details about
the meaning and transformation of local definitions.


\subsection{Equality and Constraints}
\label{sec-equality}

In order to compare the values of two expressions,
there is a predefined predicate \ccode{==}\pindex{==}\index{equality}
%\index{strict equality}\index{equality!strict}
to test the convertibility of expressions to identical data terms.
The expression $e_1 \code{==} e_2$ reduces to \code{True} if
$e_1$ and $e_2$ are reducible to identical ground data terms,
and it reduces to \code{False} if $e_1$ and $e_2$ are reducible to
different data terms.
If we ignore the strong type system of Curry,\footnote{%
Although \ccode{==} is defined like a polymorphic function,
it should be better considered as an overloaded function symbol.
This could be more precisely expressed using
type classes which might be included in a future extensions of Curry.}
we can consider the equality predicate as defined by the following rules:
\begin{curry}
C         == C        = True $\hspace{20ex}$-- for all 0-ary constructors C
C $x_1\ldots{}x_n$ == C $y_1\ldots{}y_n$ = $x_1$==$y_1$ &&$\ldots$&& $x_n$==$y_n$  -- for all $n$-ary constructors C
C $x_1\ldots{}x_n$ == D $y_1\ldots{}y_m$ = False $\hspace{15ex}$-- for all different constructors C and D
\end{curry}
For instance, consider the datatype \code{Person}
as defined in Section~\ref{ex-persons} and lists as defined in
Section~\ref{sec-datatypes}. Then the equality on these types is
defined by the following rules (where \ccode{\&\&} is the Boolean
conjunction, see Section~\ref{sec-bool}):
\begin{curry}
John      == John      = True
Christine == Christine = True
Alice     == Alice     = True
Andrew    == Andrew    = True
John      == Christine = False
$\vdots$
Andrew    == Alice     = False$\listline$
[]        == []        = True
(x:xs)    == (y:ys)    = x==y && xs==ys
[]        == (_:_)     = False
(_:_)     == []        = False
\end{curry}
This equality test, which is sometimes called
\emph{strict equality}\index{strict equality}\index{equality!strict}
and also used in functional languages,
is the only sensible notion of equality in the presence of
non-terminating functions
\cite{GiovannettiLeviMoisoPalamidessi91,MorenoRodriguez92}.
For instance, \ccode{[John]==[John]} reduces to \code{True}
and \ccode{[John]==[John,Andrew]} reduces to \code{False}.

If one expression contains free variables, they are
instantiated in order to evaluate the equality.
For instance, \ccode{[John]==x} binds \code{x} to \code{[John]}
and reduces to \code{True}, but it also reduces to \code{False}
with the bindings of \code{x} to \code{[]}, \code{(Alice:\us{})} etc.

If one is interested only in bindings for positive solutions,
i.e., reductions to \code{True}, one can also use the predefined
operation \ccode{=:=}. Conceptually, it can be considered
as defined by the ``positive'' \ccode{==}-rules:
\begin{curry}
C         =:= C        = True $\hspace{22.5ex}$-- for all 0-ary constructors C
C $x_1\ldots{}x_n$ $\,$=:= C $y_1\ldots{}y_n$ = $x_1$=:=$y_1$ &$\ldots$& $x_n$=:=$y_n$  $~~$-- for all $n$-ary constructors C$\listline$
True & True = True
\end{curry}
With these rules, \ccode{[John]=:=x} has a unique result,
i.e., \code{x} is bound to \code{[John]} so that the value \code{True}
is returned.
Since \code{$e_1$=:=$e_2$} can be interpreted as a constraint
between $e_1$ and $e_2$ that must be solved, it is also called an
\emph{equational constraint}\index{equational constraint}
\index{constraint!equational}\pindex{=:=}\index{equality!in constraints}
between the expressions $e_1$ and $e_2$.
Operationally, the equational constraint $e_1\code{=:=}e_2$ is solved
by evaluating $e_1$ and $e_2$ to unifiable data terms
and computing the unifier between these data terms.
For instance, \ccode{[John,x]=:=[y,z]} is solved by binding
\code{y} to \code{John} and \code{x} to \code{z} (or vice versa).
This is in contrast to \ccode{[John,x]==[y,z]} which is solved
by binding \code{y} to \code{John} and both \code{x} and \code{z}
to \code{John}, \code{Christine}, \code{Alice}, or \code{Andrew}.
Hence, the equational constraint yields one solution whereas
the equality \ccode{==} yields four solutions (as well as many more
non-solutions). Therefore, \ccode{=:=} can be considered
as an optimization of \ccode{==}, but it can only be used in contexts
where positive solutions are required, e.g., in conditions
of program rules.

An equational constraint could also be solved in an incremental
manner by an interleaved lazy evaluation of the expressions
and binding of variables to constructor terms (see
\cite{LoogenLopezFraguasRodriguezArtalejo93PLILP}
or Section~\ref{sec-equationsolving} in the appendix).
Note that the basic kernel of Curry only provides
strict equations $e_1\code{=:=}e_2$ between expressions
as elementary constraints. Since it is conceptually fairly easy to add
other constraint structures \cite{LopezFraguas92},
extensions of Curry may provide richer constraint systems
to support constraint logic programming applications.

As shown in the definition above, equational constraints
are combined into a \emph{conjunction} with the operator \ccode{\&}.%
\index{conjunction}\index{conjunction!concurrent}%
\index{conjunction!of constraints}\pindex{\&}
Since this operators demands that both arguments must be
evaluated to \code{True} in order to obtain any result
(otherwise, its evaluation fails),
this conjunction is interpreted \emph{concurrently}:
if the combined constraint $c_1 \cconj c_2$ should
be solved, $c_1$ and $c_2$ are solved concurrently.
In particular, if the evaluation of $c_1$ suspends
(see Sections~\ref{sec-integers} or \ref{sec-ensurenotfree}),
the evaluation of $c_2$ can proceed which may cause the reactivation
of $c_1$ at some later time (due to the binding of common variables).
In a sequential implementation, the evaluation of $c_1 \cconj c_2$
could be started by an attempt to solve $c_1$.
If the evaluation of $c_1$ suspends,
an evaluation step is applied to $c_2$.

It is interesting to note that parallel functional computation models
\cite{BreitingerLoogenOrtega95,ChakravartyEtAl98Goffin}
are covered by the use of concurrent constraints.
For instance, a constraint of the form
\begin{curry}
x =:= f t1  &  y =:= g t2  &  z =:= h x y
\end{curry}
specifies
a potentially concurrent computation of the functions \code{f}, \code{g} and
\code{h} if the function \code{h} can proceed its computation
only if the arguments have been bound by evaluating the expressions
\code{f t1} and \code{g t2}. Since constraints
can 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 \cite{ChakravartyEtAl98Goffin}.
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 \cite{Antoy97ALP,AntoyEchahedHanus00JACM},
where similar techniques for the concurrent parts are not available.



\subsection{Higher-order Features}

Curry is a higher-order language supporting common
functional programming techniques by partial function applications
and lambda abstractions. \emph{Function application}\index{function application}
is denoted by juxtaposition
the function and its argument. For instance, the well-known \code{map}
function is defined in Curry by
\begin{curry}
map :: (a -> b) -> [a] -> [b]
map f []     = []
map f (x:xs) = f x : map f xs
\end{curry}
However, there is an important difference w.r.t.{} to functional programming.
Since Curry is also a logic language, it allows logical variables
also for functional values, i.e., it is possible to evaluate the
equation \code{map f [1 2] =:= [2 3]} which has, for instance, a solution
\code{\{f=inc\}} if \code{inc} is the increment function on natural numbers.
In principle, such solutions can be computed by extending (first-order)
unification to \emph{higher-order unification}
\cite{HanusPrehofer99JFP,NadathurMiller88,Prehofer95Diss}.
Since higher-order unification is a computationally expensive
operation, Curry delays the application of unknown functions
until the function becomes known
\cite{Ait-KaciLincolnNasr87,Smolka95}.\footnote{Note that
an unbound functional variable can never be instantiated
if all program rules are constructor-based and the equational constraint
\code{=:=} denotes equality between data terms.
However, extensions of Curry might overcome this weakness
by instantiating unbound functional variables to
(type-conform) functions occurring in the program in order
to evaluate an application (as in \cite{Gonzalez-MorenoEtAl97ICLP}),
or by considering partial applications
(i.e., functions calls with less than the required number of arguments)
as data terms (as in \cite{Warren82}).}

In situations where a function is only used a single time, it is tedious
to assign a name to it. For such cases, anonymous functions
(\emph{$\lambda$-abstractions}\index{lambda-abstraction@$\lambda$-abstraction}),
denoted by
\begin{curry}
\$x_1\ldots{}x_n$->$e$
\end{curry}
are provided.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "report"
%%% End: