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

From: Michael Hanus <mh_at_informatik.uni-kiel.de>

Date: Thu, 01 Oct 2015 13:45:36 +0200

Dear Colleagues,

usually language definitions become more complex with

every new version (see the history of Java). In this sense,

I want to make an unusual proposal:

Simplify the definition of Curry

In short, I propose to remove the type "Success" from Curry.

Let me explain this proposal (which was initiated by Sergio Antoy)

in more detail.

Originally, the type "Success" was introduced in order to distinguish

Boolean expressions, which are typicially used in if-then-else,

from constraints, typically occurring in condition of rules.

Constraints are only intended to be satisfied so that they should

be never evaluated to "False". As a consequence, there are two

kinds of equalities in Curry: Boolean equality ("==") which evaluates=

to True or False, and equational constraints ("=:=") that evaluate

to "success" only (or their evaluation fails). Although there were

good reasons for this distinction ("==" is similar to functional

programming whereas "=:=" is unification like in logic programming),

it also comes with some drawbacks:

- The difference between Bool and Success is often not easy to grasp

for beginners (my experience from lectures).

- It is sometimes not obvious which kind of equality should be chosen

in a particular application.

- Standard combinators on Booleans are duplicated for the Success type

(e.g., see the library "Constraint" in PAKCS/KiCS2).

All these problems can be avoided if the type Success is removed.

As a consequence, one can drop "=:=" and make "==" a flexible

operation (currently, "==" suspends if one argument is a free

variable), i.e., one can consider "==" as a standard function

which is evaluated by narrowing. Actually, this is done in the

Curry implementation KiCS2 and it works quite well.

However, there is one argument to keep "=:=": it could be more

efficient than "==". For instance, the evaluation of

xs == ys && xs++ys == [True]

results in an infinite search space (since the first equality

is solved by binding xs and ys to Boolean lists and there are

infinitely many possibilities), whereas the constraint

xs =:= ys & xs++ys =:= [True]

has a finite search space (since the first equational constraint

binds xs and ys to the same variable). Fortunately, this operational

aspect can be hidden: if it is known that a Boolean equality *must*

be evaluated to True (and not to False), then one can replace it

by an equational constraint which simply binds one argument,

if it is a free variable, to the other. For instance, if an

equality occurs in a condition of a rule, as in

last xs | xs==_++[x] = x where x free

it can be safely transformed into

last xs | xs===_++[x] = x where x free

where "===" is the same as "=:=" but returns True (instead

of "success"), i.e., it can be considered as defined by

(===) :: a -> a -> Bool

x === y | x =:= y = True

BTW, this transformation can be done at compile time.

PAKCS and KiCS2 contain a transformation phase which

automatically does this, see the paper

http://www.informatik.uni-kiel.de/~mh/papers/LOPSTR15.html

for more technical details.

The introduction into KiCS2, which can be found at

http://www-ps.informatik.uni-kiel.de/kics2/starting.html

already explains the standard FLP features without a

reference to the type Success. Moreover, this is

implemented since some time in PAKCS and KiCS2

and we didn't get any problems with it. Of course,

for backward compatibility, the type Success and "=:="

should not be immediately removed from the implementations.

Hence, the concrete proposal is as follows:

1. Drop references to the type Success, use Bool instead.

2. Replace occurrences of "=:=" by "==" and define "=="

as a flexible function based on narrowing.

3. Add "===" as above to the prelude but don't use it

explicitly.

I hope you agree to this simplification.

Of course, I welcome any comments or objections.

Best regards,

Michael

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Do Okt 15 2015 - 15:52:45 CEST

Date: Thu, 01 Oct 2015 13:45:36 +0200

Dear Colleagues,

usually language definitions become more complex with

every new version (see the history of Java). In this sense,

I want to make an unusual proposal:

Simplify the definition of Curry

In short, I propose to remove the type "Success" from Curry.

Let me explain this proposal (which was initiated by Sergio Antoy)

in more detail.

Originally, the type "Success" was introduced in order to distinguish

Boolean expressions, which are typicially used in if-then-else,

from constraints, typically occurring in condition of rules.

Constraints are only intended to be satisfied so that they should

be never evaluated to "False". As a consequence, there are two

kinds of equalities in Curry: Boolean equality ("==") which evaluates=

to True or False, and equational constraints ("=:=") that evaluate

to "success" only (or their evaluation fails). Although there were

good reasons for this distinction ("==" is similar to functional

programming whereas "=:=" is unification like in logic programming),

it also comes with some drawbacks:

- The difference between Bool and Success is often not easy to grasp

for beginners (my experience from lectures).

- It is sometimes not obvious which kind of equality should be chosen

in a particular application.

- Standard combinators on Booleans are duplicated for the Success type

(e.g., see the library "Constraint" in PAKCS/KiCS2).

All these problems can be avoided if the type Success is removed.

As a consequence, one can drop "=:=" and make "==" a flexible

operation (currently, "==" suspends if one argument is a free

variable), i.e., one can consider "==" as a standard function

which is evaluated by narrowing. Actually, this is done in the

Curry implementation KiCS2 and it works quite well.

However, there is one argument to keep "=:=": it could be more

efficient than "==". For instance, the evaluation of

xs == ys && xs++ys == [True]

results in an infinite search space (since the first equality

is solved by binding xs and ys to Boolean lists and there are

infinitely many possibilities), whereas the constraint

xs =:= ys & xs++ys =:= [True]

has a finite search space (since the first equational constraint

binds xs and ys to the same variable). Fortunately, this operational

aspect can be hidden: if it is known that a Boolean equality *must*

be evaluated to True (and not to False), then one can replace it

by an equational constraint which simply binds one argument,

if it is a free variable, to the other. For instance, if an

equality occurs in a condition of a rule, as in

last xs | xs==_++[x] = x where x free

it can be safely transformed into

last xs | xs===_++[x] = x where x free

where "===" is the same as "=:=" but returns True (instead

of "success"), i.e., it can be considered as defined by

(===) :: a -> a -> Bool

x === y | x =:= y = True

BTW, this transformation can be done at compile time.

PAKCS and KiCS2 contain a transformation phase which

automatically does this, see the paper

http://www.informatik.uni-kiel.de/~mh/papers/LOPSTR15.html

for more technical details.

The introduction into KiCS2, which can be found at

http://www-ps.informatik.uni-kiel.de/kics2/starting.html

already explains the standard FLP features without a

reference to the type Success. Moreover, this is

implemented since some time in PAKCS and KiCS2

and we didn't get any problems with it. Of course,

for backward compatibility, the type Success and "=:="

should not be immediately removed from the implementations.

Hence, the concrete proposal is as follows:

1. Drop references to the type Success, use Bool instead.

2. Replace occurrences of "=:=" by "==" and define "=="

as a flexible function based on narrowing.

3. Add "===" as above to the prelude but don't use it

explicitly.

I hope you agree to this simplification.

Of course, I welcome any comments or objections.

Best regards,

Michael

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

- application/pgp-signature attachment: OpenPGP digital signature

*
This archive was generated by hypermail 2.3.0
: So Jul 05 2020 - 07:15:05 CEST
*