[Agda] Bug in simplification?

[Philip Wadler]

Why does the attached not work? Is there a workaround, or a repair on the
horizon? Note particularly the "1" in the error message, which appears
spurious. Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

[András Kovács]

Hi,

As far as I know, the issue is that

1. Agda elaborates pattern matching lambdas to new top-level definitions
with machine-generated names
2. Agda does not look into bodies of pattern matching functions when
checking definitional equality

Hence, Agda doesn't know that two pattern matching lambdas which look the
same in the source are equal.

People tolerate this limitation because we rarely rely on the rather
fragile intensional equality of functions. Instead we postulate function
extensionality when required.

If you'd like to have a bit more intensional function equality, you can use
top-level lemmas instead of pattern lambdas, like this
<http://lpaste.net/363727>.

If you'd like to have as much as possible intensional function equality,
you need to write all of your functions in terms of eliminators, thereby
making all of your function bodies visible to Agda, as induction method
arguments to eliminators.

Post by Philip Wadler
Why does the attached not work? Is there a workaround, or a repair on the
horizon? Note particularly the "1" in the error message, which appears
spurious. Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Philip Wadler]

Thanks, that works! My final solution is attached.

The '1' that appears in printing the function body in my original message
appears to be a bug, and should be fixed. If it's not on a list of known
bugs, what would I do to add it?

Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by András Kovács
Hi,
As far as I know, the issue is that
1. Agda elaborates pattern matching lambdas to new top-level definitions
with machine-generated names
2. Agda does not look into bodies of pattern matching functions when
checking definitional equality
Hence, Agda doesn't know that two pattern matching lambdas which look the
same in the source are equal.
People tolerate this limitation because we rarely rely on the rather
fragile intensional equality of functions. Instead we postulate function
extensionality when required.
If you'd like to have a bit more intensional function equality, you can
use top-level lemmas instead of pattern lambdas, like this
<http://lpaste.net/363727>.
If you'd like to have as much as possible intensional function equality,
you need to write all of your functions in terms of eliminators, thereby
making all of your function bodies visible to Agda, as induction method
arguments to eliminators.

Post by Philip Wadler
Why does the attached not work? Is there a workaround, or a repair on the
horizon? Note particularly the "1" in the error message, which appears
spurious. Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Ulf Norell]

You can report it by clicking the "New Issue" button here:
https://github.com/agda/agda/issues

/ Ulf

Post by Philip Wadler
Thanks, that works! My final solution is attached.
The '1' that appears in printing the function body in my original message
appears to be a bug, and should be fixed. If it's not on a list of known
bugs, what would I do to add it?
Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by András Kovács
Hi,
As far as I know, the issue is that
1. Agda elaborates pattern matching lambdas to new top-level definitions
with machine-generated names
2. Agda does not look into bodies of pattern matching functions when
checking definitional equality
Hence, Agda doesn't know that two pattern matching lambdas which look the
same in the source are equal.
People tolerate this limitation because we rarely rely on the rather
fragile intensional equality of functions. Instead we postulate function
extensionality when required.
If you'd like to have a bit more intensional function equality, you can
use top-level lemmas instead of pattern lambdas, like this
<http://lpaste.net/363727>.
If you'd like to have as much as possible intensional function equality,
you need to write all of your functions in terms of eliminators, thereby
making all of your function bodies visible to Agda, as induction method
arguments to eliminators.

Post by Philip Wadler
Why does the attached not work? Is there a workaround, or a repair on
the horizon? Note particularly the "1" in the error message, which appears
spurious. Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Philip Wadler]

Thank you. Done! -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Ulf Norell
https://github.com/agda/agda/issues
/ Ulf

Post by Philip Wadler
Thanks, that works! My final solution is attached.
The '1' that appears in printing the function body in my original message
appears to be a bug, and should be fixed. If it's not on a list of known
bugs, what would I do to add it?
Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by András Kovács
Hi,
As far as I know, the issue is that
1. Agda elaborates pattern matching lambdas to new top-level definitions
with machine-generated names
2. Agda does not look into bodies of pattern matching functions when
checking definitional equality
Hence, Agda doesn't know that two pattern matching lambdas which look
the same in the source are equal.
People tolerate this limitation because we rarely rely on the rather
fragile intensional equality of functions. Instead we postulate function
extensionality when required.
If you'd like to have a bit more intensional function equality, you can
use top-level lemmas instead of pattern lambdas, like this
<http://lpaste.net/363727>.
If you'd like to have as much as possible intensional function equality,
you need to write all of your functions in terms of eliminators, thereby
making all of your function bodies visible to Agda, as induction method
arguments to eliminators.

Post by Philip Wadler
Why does the attached not work? Is there a workaround, or a repair on
the horizon? Note particularly the "1" in the error message, which appears
spurious. Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda