[Agda] optional dot in dot patterns?

[Peter Divianszky]

On 19/11/2012 11:57, Nils Anders Danielsson wrote:
> On 2012-11-19 10:05, Peter Divianszky wrote:
>> Function calls could be recognized by checking whether there is a
>> function with that name in scope.
>
> What about shadowing?

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.

> Sometimes it matters where you put the dots. Consider the following data
> type:
>
>    data D : Set where
>      d₁ d₂ : D
>
> The following definition is OK:
>
>    foo : (x y : D) → x ≡ y → D
>    foo .d₁ d₁ refl = d₁
>    foo _   d₂ _    = d₂
>
> However, the following isn't (incomplete pattern matching):
>
>    bar : (x y : D) → x ≡ y → D
>    bar d₁ .d₁ refl = d₁
>    bar _   d₂ _    = d₂
>
> Let's add a final absurd clause:
>
>    bar : (x y : D) → x ≡ y → D
>    bar d₁ .d₁ refl = d₁
>    bar _   d₂ _    = d₂
>    bar d₂  d₁ ()
>
> Now we have foo x d₂ eq = d₂ (definitionally, for variables x and eq),
> but not bar x d₂ eq = d₂.

I see.
If dot would be optional, then one could write

    foo : (x y : D) → x ≡ y → D
    foo .d₁ d₁ refl = d₁
    foo _   d₂ _    = d₂

but also

    bar : (x y : D) → x ≡ y → D
    bar d₁  d₁ refl = d₁
    bar _   d₂ _    = d₂
    bar d₂  d₁ ()

(the second d₁ in the first alternative is automatically dotted).

Another option: use a smarter algorithm to find out that in

    foo : (x y : D) → x ≡ y → D
    foo d₁ d₁ refl = d₁
    foo _  d₂ _    = d₂

we pattern match on the second argument, and d₁ is dotted.

But at least dotted constructors could miss dots:

   data _≤_ : ℕ → ℕ → Set  where
     zero : ∀ n → zero ≤ n
     suc  : ∀ n m → n ≤ m → suc n ≤ suc m

then instead of

4≰2 : 4 ≤ 2 → ⊥
4≰2 (suc .3 .1 (suc .2 .0 ()))

one could write

4≰2 : 4 ≤ 2 → ⊥
4≰2 (suc 3 1 (suc 2 0 ()))

I guess 2 dots out of 3 could be omitted on average.