Proposal: Simplifying Curry

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

This archive was generated by hypermail 2.3.0 : Sa Dez 07 2019 - 07:15:11 CET