[Agda] optional dot in dot patterns?

Andreas Abel andreas.abel at ifi.lmu.de
Tue Nov 20 11:42:26 CET 2012

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.


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

More information about the Agda mailing list