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