rewrite and issue 1692 [Re: [Agda] aggressive with, VFPiA]
Aaron Stump
aaron-stump at uiowa.edu
Thu Jan 28 02:48:08 CET 2016
Dear Andreas,
Many thanks for the quick fix. I will try the steps you suggested, as
soon as github is operational again (there is an outage currently).
About the current master: for me, it is no trouble if I have to make
some changes from time to time with things like pragmas, in order for
the IAL to continue to check with new Agda versions. That is what I was
trying to say in my first email: of course Agda is being actively
developed and I do not demand that my library always work unchanged with
it. Only I am hoping to avoid major changes such as the one with "with"
that you fixed already now for me (I will confirm tomorrow), which break
something in a more fundamental way than infix directives and such. I
So maybe my request should have been, please to keep in mind the
development branch of the IAL for big changes:
svn co --username=guest --password=guest
https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial
Of course, I will try to do so, too, but it might take me some time (as
in this case) to upgrade and discover a problem. We'll make it work... :-)
Cheers, and thanks again for Agda,
Aaron
On 01/27/2016 04:45 PM, Andreas Abel wrote:
> 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
>>>
>>>
>>
>
More information about the Agda
mailing list