Dear Colleagues,
as a result of the constructive discussion during the last weeks,
I have updated the Curry language definition which includes
all the changes we agreed on.
As usual, you can find the new version via the Curry homepage
(
http://www-i2.informatik.rwth-aachen.de/~hanus/curry)
or directly at
http://www-i2.informatik.rwth-aachen.de/~hanus/curry/papers/report.dvi.Z.
To simplify the access to the changes for you, I summarize
the most important points (this is a long list, but most of these
points have been discussed on this mailing list):
1. Constraints are expressions from a syntactic point of view,
i.e., the curly brackets around constraints are omitted.
2. The symbol "=:=" is used for unification, i.e., the unification
of two expressions e1,e2 is written as "e1 =:= e2" instead
of "e1 = e2". The use of "=" for unification was originally
intended to be conform with unification in Prolog but causes
some trouble in the context of a Haskell syntax. On the other
hand, the use of "=:=" for unification can be also seen
as conform with Prolog since the ISO standard uses "=:="
for arithmetic equality (including the evaluation of both sides)
and several Prolog systems uses this symbol for equational
constraints.
3. The concurrent conjunction is written with the infix operator "&"
and "success" denotes the always satisfiable constraint.
Moreover, the sequential conjunction of constraints ("&>")
is added to the prelude.
4. In expressions of the form "let x1,...,xn free in c",
c must be an expression of type "Constraint".
5. The scoping rules for implicitly declared extra-variables
have been simplified (Section 2.4). Since constraints
are no longer syntactically distinguishable from other expressions,
the "smallest constraint enclosing an expression" is not
directly recognizable. Therefore, all extra-variables (identifiers
starting with an underscore) in a rule are now always considered
as declared at the top-level of the condition.
6. In conditional rules of the form "l | c = r", the condition c
is an expression of type "Constraint".
In order to be compatible with Haskell, we allow the following
syntactic sugar:
- a rule of the form "l | b = r" where b is of type "Bool" is
considered as an abbreviation for "l | b=:=True = r"
- a rule with multiple guards of Boolean type, i.e.,
l | b1 = r1
| b2 = r2
...
| bn = rn
where each bi has type "Bool", is considered as an abbreviation for
l = if b1 then r1 else
if b2 then r2 else
...
if bn then rn else undefined
(where "undefined" is a non-reducible function).
This means that Booleans guards have a sequential reading
rather than a parallel one which is reasonable for constraints.
For convenience, the function "otherwise" (=True) is predefined.
Note that this has a subtle consequence for the type inference.
In contrast to Miranda or Haskell, the type inferencer cannot
assume that the guard has always type Bool, but it must type
l | g1 = r1
| ...
| gn = rn
by typing each gi separately without any further assumptions,
yielding type ti for gi. After that, all ti must be
unifiable to either "Constraint" (default case) or "Bool".
Thus, a mixture between Constraint and Bool guards is not
allowed (see Section 2.2.2).
5. Defaults for flex/rigid: Functions of type "Constraint"
(previously: Bool) are flexible, all others are rigid by default.
There are reasonable arguments for this default and it also
simplifies the use of encapsulated search (where Constraint
functions are assumed to be the source of non-determinism).
6. The choice construct is deleted. Instead of this committed choice,
there is a new evaluation annotation "choice" which declares
a function as a committed choice function. For instance,
the indeterministic merge can be defined as follows:
merge eval choice
merge [] l2 = l2
merge l1 [] = l1
merge (e:r) l2 = e : merge r l2
merge l1 (e:r) = e : merge l1 r
This definition is simpler and really lazy in contrast to the
old use of the "choice" construct. The following operational
behavior for a function call with evaluation annotation "choice"
is informally defined as follows:
Evaluate this function call as usual (with a fair evaluation of
alternatives) but
- do not bind variables occurring in this call
- ignore all alternatives if one rule matches and its guard is
entailed (i.e., satisfiable without binding goal variables)
The first restriction is similar to the rigid annotation
but requires a rigid evaluation also for all subcalls
(as in the old "choice"). Thus, the new evaluation annotation
has the same power as the old "choice" construct but avoids
the special syntax and scoping rules in the "choice".
7. A clarification about the role of variables and functions
w.r.t. sharing introduced (2.2.1). In Section 2.3 it is added
that local variable declarations are considered as those
and not as 0-ary functions.
End of Section D.2: Remark about the necessity of sharing added.
Best regards,
Michael
Received on Do Nov 19 1998 - 10:46:00 CET