Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

2015-09-22 Thread Tobias Nipkow 
The "op" noation is idiosyncratic, but there are examples (not in individual 
formulae) where I find some such notation convenient. I would welcome Haskell's 
"(+)", but that has a problem with "(*)". Unless we can make that notation work, 
I don't think we profit much by a change. Hence I am inclined to leave things as 
they are.


Tobias

On 22/09/2015 16:21, Florian Haftmann wrote:

The »op •« is infamous. Whatever you wish instead (my personal favorite
being no special syntax at all), problems include
a) to detect unintended printing behaviour
b) a suitable migration mechanisms

Concerning b), one you could imagine things like
a) alternative declarations (infix(l/r)_new beside infix(l/r),
infix(l/r) beside infix(l/r)_old)
b) a flag to control the semantics of infix(l/r)
c) a flag combined with a data slot to modify existing mixfix
declarations afterwards also

Personally I would appreciate some move here, but this only makes sense
if we agree what the goal is and whether it is worth the effort.

Cheers,
Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Notes on GHC an mutable data structures

2015-09-22 Thread Florian Haftmann 
http://www.aosabook.org/en/ghc.html, section starting with »Crime
Doesn't Pay« – from The Architecture of Open Source Applications (Volume
2): The Glasgow Haskell Compiler

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2015-09-22 Thread Florian Haftmann 
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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

2015-09-22 Thread Florian Haftmann 
The »op •« is infamous. Whatever you wish instead (my personal favorite
being no special syntax at all), problems include
a) to detect unintended printing behaviour
b) a suitable migration mechanisms

Concerning b), one you could imagine things like
a) alternative declarations (infix(l/r)_new beside infix(l/r),
infix(l/r) beside infix(l/r)_old)
b) a flag to control the semantics of infix(l/r)
c) a flag combined with a data slot to modify existing mixfix
declarations afterwards also

Personally I would appreciate some move here, but this only makes sense
if we agree what the goal is and whether it is worth the effort.

Cheers,
Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2015-09-22 Thread 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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

2015-09-22 Thread Larry Paulson 
Is there a consensus that there is a problem with this notation? Having no 
special syntax might work, especially with jEdit, where one can click on an 
unexpected constant to see what it refers to.

Larry

> On 22 Sep 2015, at 15:21, Florian Haftmann 
>  wrote:
> 
> The »op •« is infamous. Whatever you wish instead (my personal favorite
> being no special syntax at all), problems include
> a) to detect unintended printing behaviour
> b) a suitable migration mechanisms
> 
> Concerning b), one you could imagine things like
> a) alternative declarations (infix(l/r)_new beside infix(l/r),
> infix(l/r) beside infix(l/r)_old)
> b) a flag to control the semantics of infix(l/r)
> c) a flag combined with a data slot to modify existing mixfix
> declarations afterwards also
> 
> Personally I would appreciate some move here, but this only makes sense
> if we agree what the goal is and whether it is worth the effort.
> 
> Cheers,
>   Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Definite name for case combinator on products [was: NEWS]

2015-09-22 Thread Florian Haftmann 
So, the direction is going towards prod_case.

If this is settled, the consequences are:
* Abbreviation »uncurry« will disappear again.
* Abbreviation »split« will disappear finally (using the distribution
and AFP as indicator whether this is »now« or »later«).
* Theorem names contain »prod_case« instead of »split«; the latter are
retained as aliasses, but documentation etc. is updated to prefer the
first version.
* There is no way to have something like »curry (uncurry f) = f«
printed; entering »curry (prod_case f) = f« prints as »curry (λ(x, y). f
x y) = f« by default.

Any headache with this?

Florian

Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel:
> Hi Florian,
> 
> while I very much welcome the simplified printing rules and your effort
> of unifying case_prod/split, I am not sure if adding a third alternative
> name is the way to go. The situation reminds me of the one depicted in [1].
> 
> Clearly, case_prod is the "right" name from the perspective of the
> (co)datatype package.
> 
> Dmitriy
> 
> [1] https://xkcd.com/927/
> 
> On 10.09.2015 12:02, Florian Haftmann wrote:
>> * Combinator to represent case distinction on products is named
>> "uncurry", with "split" and "prod_case" retained as input abbreviations.
>>
>> Partially applied occurences of "uncurry" with eta-contracted body
>> terms are not printed with special syntax, to provide a compact
>> notation and getting rid of a special-case print translation.
>>
>> Hence, the "uncurry"-expressions are printed the following way:
>>
>> a) fully applied "uncurry f p": explicit case-expression;
>>
>> b) partially applied with explicit double lambda abstraction in
>> the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;
>>
>> c) partially applied with eta-contracted body term "uncurry f":
>> no special syntax, plain "uncurry" combinator.
>> This aims for maximum readability in a given subterm.
>> INCOMPATIBILITY.
>>
>> This refers to e6b1236f9b3d.
>>
>> This schema emerged after some experimentation and seems to be a
>> convenient compromise. The longer perspective is to overcome the
>> case_prod/split schism eventually and consolidate theorem names accordingly.
>>
>> The next step after this initial cleanup is to tackle the »let (a, b) =
>> … in …« issue.
>>
>>  Florian
>>
>>
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] ML equality types

2015-09-22 Thread Florian Haftmann 
>> val equal: ''a -> ''a -> bool
>> val not_equal:  ''a -> ''a -> bool
> 
> As far as I know, David Matthews is doing a dictionary construction
> internally (for some years already).  So it is just a minimal form of
> Haskell-style type-class discipline.

OK, I didn't quite remember this.  So, this should be fine indeed.

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2015-09-22 Thread Larry Paulson 
Like, next week I do want to try to unify of_nat and real.
Larry

> On 22 Sep 2015, at 15:39, Tobias Nipkow  wrote:
> 
> 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.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Definite name for case combinator on products [was: NEWS]

2015-09-22 Thread Dmitriy Traytel 

Sounds good to me.

Dmitriy

On 22.09.2015 16:20, Florian Haftmann wrote:

So, the direction is going towards prod_case.

If this is settled, the consequences are:
* Abbreviation »uncurry« will disappear again.
* Abbreviation »split« will disappear finally (using the distribution
and AFP as indicator whether this is »now« or »later«).
* Theorem names contain »prod_case« instead of »split«; the latter are
retained as aliasses, but documentation etc. is updated to prefer the
first version.
* There is no way to have something like »curry (uncurry f) = f«
printed; entering »curry (prod_case f) = f« prints as »curry (λ(x, y). f
x y) = f« by default.

Any headache with this?

Florian

Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel:

Hi Florian,

while I very much welcome the simplified printing rules and your effort
of unifying case_prod/split, I am not sure if adding a third alternative
name is the way to go. The situation reminds me of the one depicted in [1].

Clearly, case_prod is the "right" name from the perspective of the
(co)datatype package.

Dmitriy

[1] https://xkcd.com/927/

On 10.09.2015 12:02, Florian Haftmann wrote:

* Combinator to represent case distinction on products is named
"uncurry", with "split" and "prod_case" retained as input abbreviations.

Partially applied occurences of "uncurry" with eta-contracted body
terms are not printed with special syntax, to provide a compact
notation and getting rid of a special-case print translation.

Hence, the "uncurry"-expressions are printed the following way:

a) fully applied "uncurry f p": explicit case-expression;

b) partially applied with explicit double lambda abstraction in
the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;

c) partially applied with eta-contracted body term "uncurry f":
no special syntax, plain "uncurry" combinator.
This aims for maximum readability in a given subterm.
INCOMPATIBILITY.

This refers to e6b1236f9b3d.

This schema emerged after some experimentation and seems to be a
convenient compromise. The longer perspective is to overcome the
case_prod/split schism eventually and consolidate theorem names accordingly.

The next step after this initial cleanup is to tackle the »let (a, b) =
… in …« issue.

Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev