Curry report updated

From: Michael Hanus <hanus_at_informatik.rwth-aachen.de>
Date: Thu, 19 Nov 1998 10:40:56 +0100

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

This archive was generated by hypermail 2.3.0 : Do Feb 01 2024 - 07:15:05 CET