Re: equality of partial applications

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Tue, 19 Jun 2012 19:27:24 +0200

On Tue, Jun 19, 2012 at 10:27 AM, Wolfgang Lux <wlux_at_uni-muenster.de> wrote:
> Sebastian Fischer wrote:

>> ignore1 _ = \x -> x
>> ignore2 _ x = x

>> MCC seems to transform ignore1 into ignore2 otherwise the failure
>> would be ignored in the first example.
>
> Yes. For the sake of efficiency, MCC always eta-expands functions as much as it can.

"It's much easier to do compiler optimizations if you don't have to
preserve semantics."
– Lennart Augustsson at CUFP'12 saying the quote was by Shapiro

>> I would prefer if both 'ignore1 failed' and 'ignore2 failed' would be
>> observably indistinguishable from 'id'.
>
> I understand that preference and it does make sense to me. Unfortunately, it is hard to reconcile with MCC's tendency to eta-expand.

In this case eta-expansion would be ok without the intensional
features of =:=. 'ignore2 failed' is observably different from id only
because =:= looks at failures under partial applications.

Incidentally, I think in KiCS 'ignore1 failed', 'ignore2 failed' and
'id' are indistinguishable.

Even if I don't use intensional features myself, they make me nervous.
Equational reasoning may brake my program in unexpected ways if I use
a library with intensional features (like the Parser library) together
with a compiler that supports them (like PAKCS or MCC.)

Sebastian

_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Jun 20 2012 - 17:58:35 CEST

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:12 CEST