Sebastian Fischer wrote:
> On Mon, Jun 18, 2012 at 9:30 AM, Wolfgang Lux <wlux_at_uni-muenster.de> wrote:
>> However, what you are expecting here is extensional equality, which is impossible to support in Curry.
>
> Not only in Curry, as it is in general undecidable..
>
>> Without modifying Curry's type system, the only alternative would be reporting a runtime error when you attempt unifying two partial applications.
>
> Yes, I would prefer a runtime error (or failure) as result of
> comparing functions which would make the difference between 'id' and
> 'map id' unobservable.
I feel somewhat sympathetic with that proposal, in particular because the result of unifying two partial applications is not very well defined. A decent optimizer might in fact notice that, e.g., (+ 1) is equivalent to (1 +) and hence transform the former into the latter, so we could have a predicate
decentCompiler :: Success
decentCompiler = (+ 1) =:= (1 +)
However, ruling out unifications between two partial applications means that we would have to rule out unifications between a variable and a partial application too; otherwise we'd become dependent on the order of evaluation. For instance
let x free in x =:= x & x =:= map id
would succeed if the two constraints were evaluated from left to right, but fail if they are evaluated from right to left. But generating a runtime error (or failure) on unifications like x =:= map id when x is a free variable IMHO is a too high price to pay (at least without support from the type system to warn about or prevent such unifications altogether).
Wolfgang
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Jun 20 2012 - 17:30:02 CEST