Infix proofs

[JacquesCarette]

In #2545 @jamesmckinna mentions

most recent (knock-on) commit exposes a slight wrinkle in the parameterization: use here of the lemma, instantiated to Setoid S arises there as (S Membershipₚ.∉[]) _ which looks... not quite right

and proceeds to abandon infix proof names because of that, and @MatthewDaggitt concurs.

I think we should separate two things:

1. the awful mess Agda makes of printing mixfix names of under-parametrized module-quantified names
2. stdlib's naming conventions

We could easily consider part 1 to be a temporary (ahem) wart that will, in time, get fixed. It sure is a pain.

But should our naming conventions be robust wrt to under-parametrization at all? It might make sense to have naming conventions that are only 'nice' when module arguments are fully applied, and no guarantees otherwise. I think we're robbing ourselves of some rather elegant syntax if things need to be always even when the number of parameters is "wrong" !!

[jamesmckinna]

In #2545 @jamesmckinna mentions

most recent (knock-on) commit exposes a slight wrinkle in the parameterization: use here of the lemma, instantiated to Setoid S arises there as (S Membershipₚ.∉[]) _ which looks... not quite right

and proceeds to abandon infix proof names because of that, and @MatthewDaggitt concurs.

@JacquesCarette thanks for the thoughtful pushback on issues raised in #2542 and the subsequent #2545 that I raised.

TL;DR:

• glad you have raised this;
• I think it's a separate issue (or two, as you point out ;-))
• I don't think we were going to easily converge on a decision/solution for v2.2, not least because having seemingly enjoyed 'easy' consensus on on lib-2.2-rc1 #2542 about this, the solution in [ refactor ] proofs under Data.List.Membership.*.Properties #2545 exposed problems which, IMHO, require more thought/discussion than could be squeezed into a release-candidate review window?

Picking up the last point at length: it was not clear to me that the 'easy' consensus (including me!) about changing the design towards a postfix, explicitly-quantified proof of x ∉ [], had stood up to examination in the 'implementing' PR. I abandoned it after I screwed up what should have been easy, namely the uncoupling of the 'refactoring' parts of that PR (now merged as #2548 ) from the 'design change' parts under discussion. It would be easy enough to raise a fresh/clean PR tackling those items, but given the mess I'd made of the commits, and @MatthewDaggitt 's insightful gloss on my rather untutored observations on the effects of the change (which made me reconsider the 'easy' consensus), I made a unilateral decision to withdraw the PR in its then-current form.

Now, I had on the originating issue, of which this is now an offshoot, and a perhaps unhelpfully more general one (I haven't "abandoned infix proof names" as such!?), commented on what I thought might be the 'ux' aspects of @mechvel 's original proposal: namely what is it that we are achieving by making x explicitly quantified in the statement/proof of the lemma at hand? Unfortunately, no-one chose to pick up those discussion points, which essentially revolve around the question, not of infix/postfix proofs per se, but about how we (choose to) 'self-document' (by the type of the lemma, or by its name? or not at all) what are essentially 'immediate proofs of contradiction', via λ(). Does making x explicit improve the library design? It seemed as though it did, but for ux reasons, as well as those @MatthewDaggitt raised about general library design considerations, I'm much less clear now about what, if anything, might be the 'right' answer, either to the specific lemma at hand, or to the issue in general.

The issue you raise here is independently interesting, but feels almost orthogonal to the original. I'll try to address it in subsequent comments. In any case, the whole discussion had been in the context of comments/possible variations on v2.2-rc1, which I personally don't think should have been held up by these more substantive, moreover 'tricky', design decisions. In like fashion, the rest of #2542 concerned issues which address long-standing gaps in the v1.* and v2.* library API, and which are also therefore, as @MatthewDaggitt pointed out, really out-of-scope for a point release version bump...

[jamesmckinna]

To address this new issue: I am not against infix/mixfix proofs! But @MatthewDaggitt 's sensible, justified objections make clear that we need to be careful how we proceed, and perhaps as you hint above, there may not be hard-and-fast rules we can stick to.

What's my 'favourite' example?
∙-cong : Congruent₂ ∙ from Algebra.Structures.IsMagma (and its inherited forms all the way down...) really should be an infix operator on proofs of the same arity and fixity/precedence as the operator _∙_ it mentions... precisely because all of its (otherwise inferrable) implicitly quantified arguments are just 'noise', obscuring the fact that proofs of equations (should!) enjoy the same 'algebra' as that of the operations they govern (there's probably a more elaborate categorical/operadic way of dressing up this intuition, but not here, not now...) cf. Larry Paulson's early work in Edinburgh LCF (pre-Isabelle, I think) on 'conversions'/'conversionals'

But then @MatthewDaggitt 's objections do bite, and quite hard, too: such 'intuition' only makes sense once the carrier and the underlying relation/underlying Setoid/IsEquivalence data has been supplied, and without it, the 'obvious' syntax seems hopelessly 'broken'.

That said, this is surely what syntax declarations are actually for in Agda: to be able to supply a surface syntax which isn't a priori typecheckable, because the dependency structure of the syntax goes against the grain of that of the underlying semantic expression of the concept...

... and in this instance, my 'preferred'/'favourite' idiomatic way to (re-)express that dependency would be as an (infix!) annotation on proof-terms, a specimen version here would be (roughly!):

syntax alg.∙-cong p q = p ∙-cong[ alg ] q

so that congruence proofs are now tagged wrt to the algebra on which they operate, but in an argument position which can easily be replaced by ∙-cong[ _ ] (or even making that a dstinct syntactic form!...) to keep the noise to a minimum?

But I'm not sure whether Agda's mechanisms can support this, either in theory, or in practice! As regarding practice, we certainly don't currently do this in stdlib, so we don't have a wealth of ux insight into the pragmatics to draw on here!

[JacquesCarette]

The reason I brought this up as an issue here and didn't really comment on the PR is that I agreed that for v2.2, what was done was best. This requires too much discussion.

Regarding the syntax of some items: one of the design decisions we could make is to explicitly declare what the convention is for each. The library used to have some items (the old <$> comes to mind) that were meant to be used on the record, which was different than most things (but I really quite liked! At least this notation is available again). What I mean is that maybe some notation is meant to be used when the module's parameters have been fully supplied, and other notation is meant to be used partially applied. Other uses may results in "a mess", but that's then the user's choosing.

Your idea wrt congruence proofs would fit into that scheme, I would think.