[Agda] Agda's syntax declaration

[Wolfram Kahl]

On Sat, Nov 04, 2017 at 10:29:41AM +0100, Ulf Norell wrote:
> Ok, let me try to be more precise. In your example you are defining a
> single thing (id)
> with multiple properties. You can read it as something like this:
> 
> ```
> id.TYPE = {A : Type} → A → A
> id.VALUE = {A} x ↦ x
> id.SYNTAX = {A} x ↦ x "∶" A
> id.FIXITY = infixl 0
> ```
> 
> Contrary to your intuition "∶" is not a thing in its own right, but simply
> a terminal symbol in
> the parsing rule for id.

Saying ``the parsing rule for id'' might be a bit misleading currently,
since ``id'' still continues to be parsed without problems.


My pragmatic recommendation for syntax declarations is
to never attach syntax to an identifier that will still be used
for other purposes, including that it needs to be visible for export.

For example, you could write:

```
id : {A : Type} → A → A
id {A} x = x

idViaColon : {A : Type} → A → A
idViaColon = id

-- the following clause augments the definition of the meta-function
-- `syntax` by one more pattern-matching clause,
-- where the type of the first argument is the meta-type `identifier`
--      ;-)
-- 
syntax idViaColon {A} x = x ∶ A


infixl 0 idViaColon
```

Then users of your library can decide whether they just want TYPE and VALUE
of `id`, and import only that, or they only want SYNTAX and FIXITY of `idViaColon`
(with the VALUE and TYPE of `id` attached), and they would then import only `idViaColon`,
or in some cases they might import both.

With that kind of usage pattern for syntax, I would not even object to
actually making the syntax declaration ``the'' parsing rule for `idViaColon`,
and thus making that identifier unavailable otherwise, except in import lists.


Wolfram