[Agda] optional dot in dot patterns?

[Peter Divianszky]

On 20/11/2012 11:42, Andreas Abel wrote:
> On 19.11.2012 15:27, Peter Divianszky wrote:
>> On 19/11/2012 14:00, Nils Anders Danielsson wrote:
>>> On 2012-11-19 13:26, Peter Divianszky wrote:
>>>> I don't see that shadowing is a problem.
>>>> If we have a pattern (f x) such that f is a function in scope, then
>>>> the compiler could replace (f x) by .(f x), couldn't it?
>>>> And I ask the same for more than one or zero arguments.
>>>
>>> Currently accepted code:
>>>
>>>    postulate
>>>      A : Set
>>>
>>>    f : Set → Set
>>>    f A = A
>>>
>>> Should A be dotted here?
>>
>> Yes, it should, imho.
>>
>> I guess shadowing is useful in the following cases:
>>
>> a) we are short of names
>> b) to make program transformation easier (moving a definition)
>> c) we would like to hide a name
>>
>> My opinion regarding these:
>>
>> a) we are short of names
>>     Is this happened ever before in Agda?
>>
>> b) to make program transformation easier (moving a definition)
>>     If we use short identifiers for general definitions or definitions
>>     with very limited scope and make definitions in the right place,
>>     this is not an issue.
>>     For example, 'f A = A' above was not defined in the right place
>>     (it is not related to the postulate 'A').
>>
>> c) we would like to hide a name
>>     I'm not sure but maybe modules and 'private' should be used for that.
>
> I think you are missing an important one
>
> d) compositionality
>
> I would not want to replace bound variables only because I add or change
> an import statement.

Good point, but d) is quite close to b) and can treated similarly.
I've had a quick look at Agda Standard Libraries which is composed of 
many modules and I tried to find cases of shadowing.

Of course I didn't found anything like

f ℕ = ℕ

or

A = ...

which would cause severe shadowing.
The closest I've found so far is in Data.Nat

-------------------------
module GeneralisedArithmetic {a : Set} (0# : a) (1+ : a → a) where

   add : ℕ → a → a
   add n z = fold z 1+ n

   mul : (+ : a → a → a) → (ℕ → a → a)
   mul _+_ n x = fold 0# (λ s → x + s) n
-------------------------

where the _+_ variable would shadow addition on ℕ, but this is defined 
*before* addition so there is no shadowing here.
The point is, that definitions which use variables like _+_ or _*_ are 
general enough that they appear before the definitions of _+_ and _*_ on ℕ.

I assume that good design prevents shadowing in complex module systems too.
Assuming this, we could take advantage of this fact like layout-rules 
take advantage of nice layout of code and force good coding standards.


> In general, I think it would be better if we were *more* explicit about
> bindings in patterns (e.g. mark each bound variable).  However, that
> would be too verbose, I guess, and too much of a culture change.

That step would make Agda a lower-level language in my opinion.

Cheers,
Peter