rewrite and issue 1692 [Re: [Agda] aggressive with, VFPiA]
Andreas Abel
abela at chalmers.se
Wed Jan 27 23:45:52 CET 2016
Dear Aaron,
you are welcome! Your agda files should now check again with the
current maintenance version (2.4.2.6)
https://github.com/agda/agda/tree/maint-2.4
Get it with
git clone https://github.com/agda/agda.git
cd agda
git checkout maint-2.4
make install-bin
After that, you can use agda-2.4.2.6 on the command line or in emacs
M-x agda2-set-program version RET 2.4.2.6 RET
Please confirm things work again for you.
Note that your files do not check on current master (could be released
as agda-2.5). This is due to changes in the operator parser. Also,
some COMPILED pragmas have to be removed.
Please evaluate the amount of breakage on master with
git checkout master
make install-bin
which gives you a new version of agda (no version appended) which you
activate with
M-x agda2-set-program version RET RET
(always assuming .cabal/bin is in your PATH).
Personally, I oppose the new operator parser, but please form your own
opinion. It will likely be released anyway, so if you can add the
necessary fixity declarations before printing of your book, this might
be advisable. Otherwise, try to protest again on this list.
Cheers,
Andreas
On 27.01.2016 21:54, Aaron Stump wrote:
> Dear Andreas,
>
> Thanks for your fast, gracious, and also funny reply. Sorry I did not
> manage to check on this earlier when you called for comments on the new
> "with". I should have done that. I really appreciate that you agree to
> do something to change the funny new behavior of rewrite. I'll watch
> for an update about this once the decision has been reached on the exact
> fix.
>
> Cheers,
> Aaron
>
>
>
> On 01/27/2016 02:16 PM, Andreas Abel wrote:
>> Dear Aaron,
>>
>> thanks for your message and alerting us of more breakage. The change
>> of `with` was triggered by
>>
>> https://github.com/agda/agda/issues/1692
>>
>> where `rewrite` failed to meet the expectations. The new with/rewrite
>> fails to meet yours and is apparently not backwards compatible.
>> However, this unfortunately only surfaced after the merge. It would
>> have been helpful if you had responded to my earlier message
>>
>> https://lists.chalmers.se/pipermail/agda/2015/008202.html
>>
>> where I asked for feedback on the new with. Moreover, the plans to
>> change with/rewrite "have been on display at your local planning
>> department in Alpha Centauri for fifty of your Earth years so you’ve
>> had plenty of time to lodge any formal complaints and its far too late
>> to start making a fuss about it now." :) [D. Adams]
>>
>> More seriously, you complaint is a reasonable one and something has to
>> be done about this. It seems to be easiest to change the rewrite
>> tactic such that
>>
>> lemma f a p rewrite p = p
>>
>> behaves like
>>
>> data Protect {a} {A : Set a} : A → Set where
>> protect : ∀ x → Protect x
>>
>> lemma : ∀ {A : Set} (f : A → A) (a : A) (p : f a ≡ a) → f (f a) ≡ a
>> lemma f a p with protect p | f a | p
>> ... | _ | _ | refl = p
>>
>> which works around the more aggressive with with the just invented
>> Protect Pattern (TM) (C) Andreas Abel, Gothenburg University, 2016.
>>
>> This change would unfix issue 1692 but hopefully fix both your book
>> and Wolfram Kahl's code.
>>
>> Comments, anyone?
>>
>> Cheers,
>> Andreas
>>
>> On 27.01.2016 19:52, Aaron Stump wrote:
>>> Dear Agda developers,
>>>
>>> Starting in Agda version 2.4.2.5, the abstraction performed by "with"
>>> has (as the CHANGELOG tells us) become more aggressive. I am sure you
>>> have good reasons for this change, but are you aware that you have made
>>> it impossible to rewrite with the same assumption twice? Consider this
>>> self-contained example:
>>>
>>> module test where
>>>
>>> data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
>>> refl : x ≡ x
>>>
>>> {-# BUILTIN EQUALITY _≡_ #-}
>>> {-# BUILTIN REFL refl #-}
>>>
>>> lemma : ∀ {A : Set}(f : A → A)(a : A) → f a ≡ a → f (f a) ≡ a
>>> lemma f a p rewrite p = p
>>>
>>> With previous versions of Agda, this would be fine. But starting with
>>> 2.4.2.5, this does not type check. If we put a hole on the right-hand
>>> side of the sole equation for lemma, we will see this goal:
>>>
>>> Goal: f a ≡ a
>>> ————————————————————————————————————————————————————————————
>>> p : a ≡ a
>>>
>>> The "rewrite p" directive has actually been applied to rewrite the type
>>> of p itself, rendering it trivial and hence useless. This is a real
>>> problem. I have maybe 25 places in the Iowa Agda Library that have been
>>> broken by this. I don't mind fixing them, but I think this is a major
>>> flaw in the new way "with" works. One should be able to reuse
>>> assumptions. For the particular example above, I actually am struggling
>>> to find any workaround. How would you prove this? Maybe inspect on
>>> steroids is supposed to be used? For what I have done, usually inspect
>>> has been enough. But being able to apply an assumption twice with
>>> rewrite seems pretty fundamental. This is not linear logic!
>>>
>>> There is a second issue I want to raise. As you know (since Jesper and
>>> Ulf wrote me very helpful and quite detailed reviews), I am bringing
>>> out, with ACM Books, a textbook called "Verified Functional Programming
>>> in Agda" (VFPiA) this year. The book is in the very last stages of
>>> proofs. In the book, I refer readers to Agda 2.4.2.2 and IAL release
>>> 1.2:
>>>
>>> svn co --username=guest --password=guest
>>> https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial-releases/1.2
>>>
>>> So, certainly the book is usable. But this release does not check with
>>> Agda 2.4.2.5. Furthermore, some of what I say in the book is
>>> invalidated by the fact that we cannot rewrite twice with the same
>>> assumption.
>>>
>>> Of course, whether the book is successful or not is not your
>>> responsibility, though by reviewing it for me, Ulf and Jesper have made
>>> some investment in its success. But if you want to take advantage of my
>>> efforts here to help spread Agda to new users, it would be really a good
>>> idea if releases of Agda were compatible with IAL version 1.2. I do not
>>> do anything very exotic. If there are changes to compiler pragmas, that
>>> is fine. And of course, I hardly expect you to limit yourself to back
>>> compatibility with my library. But if you could at least consider
>>> whether changes you make are breaking this library (and hence, to some
>>> extent, breaking VFPiA), I would appreciate it, and I hope it would help
>>> the broader Agda community.
>>>
>>> Best wishes,
>>> Aaron
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list