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

From: Julio Mariño <jmarino_at_fi.upm.es>

Date: Fri, 9 Oct 2015 15:02:13 +0200

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

Date: Fri, 9 Oct 2015 15:02:13 +0200

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:

--

Julio Mariño

Babel research group

Universidad Politecnica de Madrid

Received on Do Okt 15 2015 - 17:15:50 CEST

*
This archive was generated by hypermail 2.3.0
: Mi Aug 05 2020 - 07:15:04 CEST
*