> Am 07.10.2015 um 20:14 schrieb Michael Hanus <mh_at_informatik.uni-kiel.de>:
>
>>> 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
Interesting. I guess that behavior doesn't extend to floating point numbers, though. :-)
> 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.
Sounds reasonable to me.
Now what about a slightly different plan: To preserve compatibility with existing code, we could get rid of the type Success by adding a type synonym
type Success = Bool
to the Prelude. We could continue using (=:=) as the name of the unification operation, but it would now have type a -> a -> Bool.
Wolfgang
_______________________________________________
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