[ style ] `syntax` declarations: to be or not to be?

[jamesmckinna]

So I couldn't help noticing, while trying to figure out the merge conflicts, that @shhyou 's original proofs made extensive use of the ... ≈[ ... ] ... syntax, whereas the proofs in this PR reinstate the explicit unfolding of that syntax into cast ... ... ≡ ... form.

Is that a Good Idea, or a Bad One?

Otherwise put: is it a style-guide/library-design precept that we don't use syntax explicitly in library modules?

Originally posted by @jamesmckinna in #2431 (comment)

I'm conscious that many/several aspects of syntax declarations (eg we can't really deprecate them, only decline to export them publicly) make their use perhaps more 'controversial'/less straightforward in stdlib library modules than elsewhere:

• avoiding using them is 'more robust', but harder to read (otherwise we wouldn't introduce them?!)
• using them is 'more abstract', so avoiding using them exposes implementation details, which may or may not be a good thing, eg

  ∃-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
  ∃-syntax = ∃
  
  syntax ∃-syntax (λ x → B) = ∃[ x ] B

  means that I don't need to see the LHS implementation of what is otherwise, less or more 'opaquely`, some sort of binding syntax,
  but I don't really need to care what that might be... while others seem actively to avoid using them...
• more/less 'ink': I follow Wadler in favouring less; truly Less is More here ;-)
• prefix/infix, the eternal debate...
• ...

Accordingly:

• should we have a policy?
• what should it be?
• how would it cash out in practice for Vec.Properties: drop eq parameter when it is a property (v3.0 changes) #2431 for example? (It might be good to decide these things before attempting to resolve the merge conflicts, as above...)

[MatthewDaggitt]

My opinion is that I think we should encourage the use of the reasoning syntax in library modules... Maybe I've misunderstood though?

[jamesmckinna]

D'oh thanks @MatthewDaggitt total 🤦 on my part.

Of course you're right (the exception being the Permutation combinators... ;-)), I was more thinking of ∃-syntax etc. where there seems to be 'nice' syntax that then isn't really used anywhere (I've done do, but often wondered whether I should).

The 'combinatory' names under Relation.Unary are another example where 'syntax', broadly understood, becomes more a question of taste (it's not to your taste, that seems clear!).

I suppose it might be seen as making the dependency graph 'thicker', if not actually more complex. There was also issue #595 about Relation.Definitions / Algebra.Definitions even unto the use of terms such as Commutative etc.

Aside from Reasoning, it seems as though there's a similar reluctance to use the 'notational' syntax that the library offers. It may just be a Fairbairn threshold kind of question... perhaps some of the notations haven't really earned their place in terms of power-to-weight ratio?

[MatthewDaggitt]

Ah right, other syntax declarations. You're right, I'm less convinced by them, but maybe that's because I haven't been brought up in the schools of logic/computer science that make use of them extensively...

[jamesmckinna]

And as to Reasoning proofs, I've also wondered in the past #2629 about whether they can somehow be sensibly 'normalised' behind the scenes, but subject to @JacquesCarette thought that we should have an interaction surface which (somehow!?) supports all the layers of surface syntax through to semantics...

[jamesmckinna]

But for now, I think that this can close, without the need for any explicit policy/change.