My position on this issue, in short, would be:
- I agree with eliminating the Success type as it was just a subtype of
Bool and making it a separate type led to the proliferation of innecessary
entities, as Occam would say.
- However, I prefer to let the programmer choose between narrowing-based or
constraint solving-based implementations of predicates. While the choice
may be simple for the special case of predefined equality of first-order
values, I do not think that generalizes well for other predicates or for
nonstandard definitions of equality.
- Allowing the automatic replacement of narrowing-based predicates by their
analogues based on constraint solving, when available, should be a compiler
optimization option.
Best regards and thanks for the initiative.
On Thu, Oct 1, 2015 at 1:45 PM, Michael Hanus <mh_at_informatik.uni-kiel.de>
wrote:
> 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
>
--
Julio Mariño
Babel research group
Universidad Politecnica de Madrid
Received on Do Okt 15 2015 - 17:15:50 CEST