[Agda] optional dot in dot patterns?
Peter Divianszky
divipp at gmail.com
Mon Nov 19 13:26:25 CET 2012
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.
More information about the Agda
mailing list