Some lemmas related to renamings and substitutions

[nad]

@jamesmckinna noticed a lack of lemmas relating renamings and substitutions, and I added some.

[jamesmckinna]

Regarding variables etc, indeed Nisse's original contribution from 10+ years ago might benefit from a little modernisation... I am grateful to him for the original contribution, and his response to my recent prompting for extensions... and I hope to return to work on this once I am back from Easter in Germany.

[jamesmckinna]

Hmmm... I've let 6 months elapse since I last commented, much less looked at (@MatthewDaggitt 's comments on) the PR. There's actually quite a lot of work to do to bring this in line with the rest of the library (plus not wishing to break any client code of @nad 's), so it'll be a while before I can get back properly to this.

[MatthewDaggitt]

Okay have cleared the v2.0 milestone.

[jamesmckinna]

@MatthewDaggitt @nad I'm sorry that I have let this one completely slide off my worklist, in favour of a thousand other distractions.

I understand the stdlib maintainer(s)'s desire to rectify the many choices in this module, and to its status even as a module in the library at all. I wonder if the best way to proceed might be to:

• [x] to do the minimum of 'cosmetic' work on style etc. that Matthew has already identified (in the interests of closing this sooner rather than later)
• [ ] regarding its status as a contribution to the library, would a compromise (sensible/defensible or otherwise) be to suggest that it move, wholesale, to the README hierarchy instead, as an exemplary instance of the use of Fin in modelling de Bruijn-/McBride-style approaches to binding (a distinct mode of use not necessarily congruent with the main aims and objectives of the 'official' library), with corresponding deprecations of the module under src?

I realise that the second suggestion may be controversial/unhelpful to the discussion, but it would (at least) avoid any complicated issues about any proposed reorganisation of the very highly ramified internal module structure already present (which I assume, perhaps wrongly, is a historical artefact of limited-resource typechecking from early in Agda's history... or else a very disciplined approach to abstraction/modularisation which definitely does not sit easily with the style of the rest of stdlib)

Let me know your thoughts.

[jamesmckinna]

Oh ****! Sorry! I have screwed things up again. Can a rebase get us out of this? Or what? :facepalm: Or fast-forwarding the branch on GitHub directly, and then recommitting the new changes? Oh, sorry sorry sorry sorry sorry...

[gallais]

Fixed by:

• returning to Nisse's last commit on this branch
• cherry-picking your two last commits

git checkout renamings_and_substitutions
git reset  3ec8125b45558731d2b92c83c14d147bc046e34e  --hard
git cherry-pick 4145020d2d915b2c9df3137eb35c1e6707768a25
git cherry-pick 99c30022e858e000b9f93d9f9a09b524b843c70e

and then force-pushing the result.

[nad]

• [ ] regarding its status as a contribution to the library, would a compromise (sensible/defensible or otherwise) be to suggest that it move, wholesale, to the README hierarchy instead, as an exemplary instance of the use of Fin in modelling de Bruijn-/McBride-style approaches to binding (a distinct mode of use not necessarily congruent with the main aims and objectives of the 'official' library), with corresponding deprecations of the module under src?

Note that the modules under README are not exported. The module Data.Fin.Substitution.Example could perhaps be turned into a README module.

I realise that the second suggestion may be controversial/unhelpful to the discussion, but it would (at least) avoid any complicated issues about any proposed reorganisation of the very highly ramified internal module structure already present (which I assume, perhaps wrongly, is a historical artefact of limited-resource typechecking from early in Agda's history... or else a very disciplined approach to abstraction/modularisation which definitely does not sit easily with the style of the rest of stdlib)

Is this remark in reference to the various record types in Data.Fin.Substitution and Data.Fin.Substitution.Lemmas? I don't recall that the design was influenced by any performance problems.

[jamesmckinna]

Regarding the various record type/module definitions in Data.Fin.Substitution and Data.Fin.Substitution.Lemmas: indeed, this structuring is one of the things which marks these modules as (dramatically) distinct from others in stdlib, and for a long time at least for me, were a considerable barrier to understanding. I had (mistakenly) presumed that they had been introduced in order to manage (time/space) complexity of type-checking, rather than for any other (good) software engineering reasons. Happy to leave all this alone!

Regarding @MatthewDaggitt 's suggestion of refactoring those modules to make heavier use of variable declarations, I'd be happy to leave that for now, but when I have resources to I return to this, I'll revisit that decision ;-) DONE now ;-)

Regarding moving *.Example to README.*, I think that that is in line with existing stdlib guidelines. PROPOSAL: that we do indeed do this as part of this PR, deprecating the old *.Example module.

[jamesmckinna]

Hmm, I now do have commits which

• [x] do the variable refactoring
• [x] deprecate Data.Fin.Substitution.Example in favour of README.Data.Fin.Substitution.UntypedLambda
• [x] some other, more cosmetic, changes

but.. having trouble pushing them to agda/renamings_and_substitutions ... not quite sure what's happened here, but will hopefully update soon.

UPDATED: not sure about the merge conflict, which then needing resolving with a somewhat anachronistic bit of time-travel for CHANGELOG, but otherwise OK. Hopefully this is done now!

UPDATED: for some (!?) reasons, CHANGELOG has picked up some spurious out-of-order commits from earlier PRs which nevertheless are consistent with the current state of master. Is it safe to remove them from this PR, for the sake of the overall history? Or leave them in, as they do not conflict, or ...?

[jamesmckinna]

Will look at merge conflicts this week.

[MatthewDaggitt]

Note that the modules under README are not exported. The module Data.Fin.Substitution.Example could perhaps be turned into a README module.

Yup agreed. I think moving the Example to README is sufficient, so merging in once the tests pass.