Hi Wolfgang,
thanks for your interesting remarks. I include my comments below.
On 10/06/2015 11:32 AM, Wolfgang Lux wrote:
> I'm a bit undecided on this one. Personally, I like the fact that functions with result type Success are the equivalent of predicates in Prolog in that they can either be satisfied or fail (whether finitely or by non-termination). Using Bool instead of Success could allow distinguishing finite failures from non-termination. However, I'm also a bit wary of introducing a new issue with guards and if-then-else cascades where people could be confused why the else case of a conditional or the remaining guards of a definition are not chosen. E.g., given a simple (directed) graph
> data Corner = E1 | E2 | E3
> edge E1 E2 = True
> edge E2 E3 = True
> the (naive) definition
> connected e1 e2
> | edge e1 e2 = True
> | otherwise = let e3 free in edge e1 e3 && connected e3 e2
> will not work as expected (no result rather than True for edge E1 E3) because the otherwise guard will never be evaluated. To work you'd have to change edge into a total function first. With the Success type this error could not happen because you can have at most one guard of type Success and you can't you if-then-else either.
I agree that this might lead to some unexpected behavior, and such kind
of examples were the reason why I was in favor of "Success" for a long
time. On the other hand, now I think that the complications
of two similar types outweigh a simpler design. For instance,
we faced problems (in program transformations) where one does
not know the type of a condition (Bool or Success). Moreover,
there are ways to transform Success values into Booleans
(e.g., "successvalue &> True") so that newbies might also
make similar mistakes also in the presence of Success.
>> 2. Replace occurrences of "=:=" by "==" and define "=="
>> as a flexible function based on narrowing.
>
> I like the idea of defining (==) as a flexible function. In particular, this feels much more natural in the context of an implementation with type classes, where (==) would become a user defined function for most types anyway. It would require a lot discipline from the user (or some compiler magic) to make all instances rigid instead. There is an issue with the equality on the built-in types Char, Int and Float. We could either keep equality rigid for those functions or solve equality by unification for these function but loose completeness (unless the implementation supports disequality constraints).
Yes, this is a good point. KiCS2 has a flexible (==) also for Int and
Char, whereas the current version of PAKCS is flexible on user-defined
types but suspends on Ints and Chars. In this way, PAKCS is less
complete than KiCS2.
> Anyway, whatever change is made here should be extended to the polymorphic ordering function compare :: a -> a -> Ordering as well.
Good point. KiCS2 already does this:
> kics2
...
Prelude> solve $ 1<x && x<=3 where x free
{x = 2} True
{x = 3} True
In general, I think that all functions should be flexible except
ensureNotFree and the case construct. (I must admit it was a long
way for this insight...)
> However, I'm afraid that replacing (=:=) by (==) everywhere and having the compiler automatically convert (==) into (=:=) with a transformation as outlined in the LOPSTR paper is a non-starter for me.
> ...
> So, while I understand the problem with two different equality operators in the beginning, I'd prefer to keep them, since I think it saves a lot of problems in the long run if the user remains in control of whether an equality is solved by unification or by narrowing and does not depend on somewhat brittle program transformations by the compiler.
I agree to keep the unification operator in the language definition,
but with the new name/type (===) :: a -> a -> Bool.
As you said, one does not want to depend on a tool
where one knows what is necessary to write efficient programs.
However, for newbies it might be easier to use one equality operator
only. In some sense, (===) is just an optimization of (==):
(==) is complete but sometimes the search space is too big,
so it can be reduced by unification. From a declarative
point of view, there is no need for (===). From my point of view,
this is related to strictness annotations or "seq" in Haskell:
usually, we don't teach it to beginners, but it is good for
advanced programmers.
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 - 17:15:50 CEST