rewrite and issue 1692 [Re: [Agda] aggressive with, VFPiA]

Andreas Abel abela at chalmers.se
Thu Jan 28 11:56:18 CET 2016 

Dear Aaron,

I think I saw a unicorn last night.  (github has a sense of humor.)

If you add a file name e.g. "everything.aga" which imports all the files 
in your ial development, we could add running agda on "everything" to 
the testsuite, or to a bigger testsuite we run from time to time.

Cheers,
Andreas

On 28.01.2016 02:48, Aaron Stump wrote:
> 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
>>>>
>>>>
>>>
>>
>

-- 
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