[isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]

[Tobias Nipkow]

Dear Florian,

I get the definite impression that the whole operation is out of proportion wrt 
the benefits. As far as I can tell, the result is a unification of two 
previously distinct constants, split and prod_case. I must confess that this 
duplication has never bothered me. Now the eta-contraction machinery needs to be 
revised, possibly resulting in a new syntactic constant, which is a further 
complication.

I would prefer to leave things as they are now. That print translation is ok and 
you would be moving the complications elsewhere. We really have more important 
issues to work on.

Tobias

On 22/09/2015 16:17, Florian Haftmann wrote:
> The situation turned out more complicated than anticipated: implicit
> eta-contraction happens at a rather late level in the printing machinery
> using a print translation. Hence, any countermeasure must act on the
> same (or a later level). However in the ecosystem as it is today, it
> seems better to do such transformations at the uncheck level, i.e. quite
> close to the logic.
>
> For the moment, I installed the print translation from e6b1236f9b3d
> again to retain the previous behavior in af7bed1360f3. Please report
> remaining suspicious behavior.
>
> To get ahead from there, I need to understand more about eta-contracted
> printing.
>
> According to my current understanding, this has been introduced once to
> produce less surprises if proof tools perform spontaneous eta-expansion
> (please correct me if this is wrong).
>
> To get more fine-grained control there, I can foresee two approaches:
> a) Move the eta-contract machinery to the uncheck level also.
> b) Provide a special syntactic marker which is »syntactic identity« but
> does not perform eta-contraction on its immediate argument. This would
> allow uncheckers to protect certain abstractions using this marker.
>
> b) seems preferable, since there is less risk to produce unexpected
> deviations from current printing without being noticed.
>
> Comments?
>
> 	Florian
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150922/a6613fd1/attachment.bin>