- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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

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
: Fr Jan 24 2020 - 07:15:04 CET
*