Use -local consistently for properties

[gallais]

In Data.List.Properties we use

• map-id₂ : All (λ x → f x ≡ x) xs → map f xs ≡ xs
• map-cong₂ : All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
• (we do not have map-compose₂)

I think that we should instead use the -relative suffix introduced in #510

[MatthewDaggitt]

What does relative refer to?

[gallais]

The fact the equality constraint is relative to a specific domain (in order to be
as tight a constraint as possible) rather than absolute.

[MatthewDaggitt]

Hmm looking at this again, I'd probably prefer the prefix -locally (or -local) instead of -relative, as in the equality constraints hold locally. Thoughts?

[JacquesCarette]

To be honest, I don't like either -locally or -relative. Isn't this rather a 'lifting' property? You're lifting an equality to hold at a list. In some ways, this is a generalization of ap.

[MatthewDaggitt]

So map-id-lift? I like it better than -relative but less than -local. I'd be fine with it though....

[MatthewDaggitt]

Going to leave this out of v1.0, as I don't think we've reached consensus yet.

[MatthewDaggitt]

@jamesmckinna thinks the suffix should be at e.g. map-id-at

After discussion we're going with local

[jamesmckinna]

Is it the case, for Lists at least, that the 'global' property map-id is (definitionally equal to; or merely equivalent to?) \forall xs \r (map-id-local xs) (modulo the actual arguments in order to fix the property)?

That is, do we uniformly have that property is All (property-local) for propertys of interest? Should we?

[jamesmckinna]

@MatthewDaggitt this could also be linked to issue #509 (or at least, to a single PR which will knock them both off). You or me?

[MatthewDaggitt]

Is it the case, for Lists at least, that the 'global' property map-id is (definitionally equal to; or merely equivalent to?) \forall xs \r (map-id-local xs) (modulo the actual arguments in order to fix the property)?

No it's not. And I'm not sure that it is desirable as the local property requires an intermediate proof of the predicate All. I don't think we should construct it just for the sake of destructing it again.

@MatthewDaggitt this could also be linked to issue #509 (or at least, to a single PR which will knock them both off). You or me?

It would be great if you could to tackle this while you're fixing #509 👍

[jamesmckinna]

I think this bit of PR #1822 is now ready.

[jamesmckinna]

I was too hasty. There is a very large raft of updateAt-* properties, each with a -relative version, in:

• Data.Vec.Properties
• Data.Vec.Functional.Properties
• Data.List.Relation.Unary.All.Properties

Turning to those Done now.
EDITED: and interestingly, those do use the 'all -local implies -global' idiom... except one, which I changed for the sake of (?) uniformity.

[jamesmckinna]

Updated CHANGELOG.

[jamesmckinna]

Problem: type of map-updateAt in Data.Vec.Functional.Properties is in fact the 'local' statement, not the 'global' as suggested by the name...
Solution: it's a leaf node in the dependency graph. Will change name, and add new 'global' definition. Interesting knock-on viscosity: can't be captured by a mere deprecation warning!

[jamesmckinna]

Is this issue now closed, or does there need to be an addition somewhere (HACKING?) to document the intention behind the name change?

[MatthewDaggitt]

I guess if you're keen you can add a note to the following?

https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md#naming-conventions

[jamesmckinna]

I'll ponder what would be the most helpful way to introduce, exemplify, and reinforce the new agreed convention. But it seems 'small' compared to the gross-scale global conventions listed there. Too much thinking required perhaps!

[jamesmckinna]

So: I think the issue/discussion of how to document the various already-merged PRs in HACKING, can be deferred to v2.1. I can't organise my thoughts properly about the right narrative approach here.

[MatthewDaggitt]

Opened #2109 to knock this off as it's definitely low hanging fruit.

[jamesmckinna]

OK, but I'll pass the baton on this one :-(