[Agda] optional dot in dot patterns?

[Andreas Abel]

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.

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.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/