Feature request: 'computed patterns'

[jamesmckinna]

Feature request: 'computed patterns'

[jamesmckinna]

Very interesting to learn these details, @andreasabel .
Unfortunately, your suggestion may require me to double-down on the request, in order to include syntax declarations whose LHS are/evaluate to patterns... would that be possible/desirable? UPDATED: on reflection, is this in fact a distinct feature request (syntax declarations whose LHS are in pattern form should be understood as defining pattern synonyms in their own right for the corresponding RHS) which could be uncoupled from the one above (and even be implemented first)?

Use case: suppose I have an infix constructor _⊗_ for eg transitivity of a relation R, such as

_⊗_ : R a b → R b c → R a c

but there are times when I might wish, during pattern matching, to expose the 'middle' argument b explicitly...
At the moment, I can suffer by writing _⊗_ {b = b} aRb bRc as a pattern, or I can simply write

infix ... _⊗[_]_
pattern aRb ⊗[ b ] bRc = _⊗_ {b = b} aRb bRc

because untyped pattern syntax won't care about the ill-typed out-of-order arguments (I'm ignoring any fastidiousness about putting the implicit arguments in, for completeness' sake, and in the event I might actually need to refer to them by name, as well).

I'm tempted to argue, from a ux point of view, that this ought to be a common case for 'informal' mathematical notations... and so want not to oblige the user to degrade immediately to some horrible prefix combination of (named) implicits and explicit arguments... (?)

But if pattern synonyms must be declared typed, do I now need in fact to make the above a syntax declaration instead, to obtain out-of-order binding of the telescope... and currently, IIUC, agda won't accept (the RHSs of) syntax declarations as potential pattern synonyms...?

Sorry if my ignorance of agda internals (and hence, at the moment, it's unlikely that I would be in a position to raise a PR solving these problems... :-() leads me to 'unreasonable' demands from a user/ux point of view, but... 'feature request' ... leading to feature creep ;-)

[andreasabel]

@UlfNorell : The milestone 2.6.5 seems bold given that pattern synonyms currently only exist on the level of abstract syntax, but evaluation is in internal syntax. (We certainly do not want fake evaluation on the AST.)
A prerequisite for this feature seems to move pattern synonyms to internal syntax, e.g., by finishing the stalled PR

• #4680

[andreasabel]

Interesting observation, James @jamesmckinna !
So to get typed pattern synonyms, we would also need some kind of "simultaneous telescopes".

[jamesmckinna]

Not sure I quite understand the idea of

... to get typed pattern synonyms, we would also need some kind of "simultaneous telescopes".

Is this to handle the out-of-order behaviour currently achievable with pattern and syntax? One telescope for the 'correct' order, and one for the 'permuted' user-supplied version? I hadn't imagined that that would be necessary? (But then, I'm not really sure what would be required... ;-))