Proposal for syntax changes in Curry

From: Michael Hanus <hanus_at_informatik.rwth-aachen.de>
Date: Thu, 22 Oct 1998 13:32:22 +0200

Dear Colleagues,

after a discussion with different people about some syntactical
aspects of Curry (see also Sven Panne's email of Feb. 9),
Herbert Kuchen and I want to propose a slight change in
the syntax for constraints in Curry. The main point is to get
rid of the special syntax for constraints (currently: enclosing
with curly brackets) and consider constraints as expressions
of the special type "Constraint". This simplifies the overall
syntax of Curry and avoids the syntactic conflict of the
current constraint notation and Haskell's record update syntax
(compare Sven Panne's email of Feb. 9). Our detailed proposal
and its consequences are discussed in the following.

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.

4. In expressions of the form "let x1,...,xn free in c",
   c must be an expression of type "Constraint".

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

   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 assume
   an unknown type and performs the inference. If this unknown
   type is not further restricted (i.e., remains polymorphic),
   it is specialized to "Constraint", otherwise it must be
   either "Constraint" or "Bool". Although this could lead
   to another typing than in Haskell, it seems to be not a
   problem in practice (deduced from many examples that I checked).
   Furthermore, one could always add a type signature.

5. Defaults for flex/rigid: Functions of type "Constraint"
   (previously: Bool) are flexible, all others are rigid by default.
   From the different examples I have, this default is reasonable
   (compare also my email of May 6) and also advantageous in
   combination with encapsulated search.

If nobody has serious objections against these changes,
I'll include it in the next version of the Curry report.
The necessary changes for the already existing implementations
should be quite small.

Best regards,

Michael
Received on Do Okt 22 1998 - 14:36:00 CEST