[Agda] Should not _ patterns be resolvable by inaccessible patterns?

[Andrea Vezzosi]

The need for "._" is certainly something that puzzles people learning
Agda, this change would help for that.

It makes "_" just a bit more special which might make it less
intuitive in other ways, but as long as it's a backwards compatible
change I think it's a good one.

Do the dot patterns affect the generated case splitting tree?
If so some proofs might break.

Best,
Andrea

On Mon, Jul 6, 2015 at 10:25 AM, Andreas Abel <abela at chalmers.se> wrote:
> P.S.: The standard library checks fine if one let _ stand for ImplicitP.
>
>
> On 06.07.2015 09:33, Andreas Abel wrote:
>>
>> If you define transitivity of propositional equality without hiding
>> value arguments, you have to explicitly choose where to put the dots:
>>
>>    transV1 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
>>    transV1 _ ._ ._ refl refl = refl
>>
>>    transV2 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
>>    transV2 ._ _ ._ refl refl = refl
>>
>>    transV3 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
>>    transV3 ._ ._ _ refl refl = refl
>>
>> With hidden arguments, you need not care:
>>
>>    transH : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
>>    transH refl refl = refl
>>
>> Of course, when giving the hidden arguments, it is the same as for
>> visible arguments:
>>
>>    transH1 : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
>>    transH1 {a = _}{b = ._}{c = ._} refl refl = refl
>>    ...
>>
>> The user has more flexibility when an argument is hidden.  When an
>> argument is given, the user has to actively make a decision whether a
>> pattern must be a dot pattern or must not be one.  There is no "I don't
>> care, please figure it out for me" as there is for hidden arguments.
>> This seems to be a mismatch.
>>
>> I think it would be simpler for the user if pattern "_" stood for "don't
>> care" rather than "unnamed variable".  The need for writing "._" would
>> vanish.
>>
>> Does anything speak against this change?  Is there a situation where it
>> is essential to tell Agda not to let something be a dot pattern in order
>> for type-checking to succeed?  (In the end this could still be done by
>> writing a named variable instead of _!)
>>
>> Internally, Agda has four kinds of trivial patterns:
>>
>>    DotP       ._ is (DotP MetaVariable)
>>    VarP       x  is (VarP "x") where x cannot be "_"
>>    WildP      _  is WildP
>>    ImplicitP  the user wrote no pattern (argument is hidden)
>>
>> The change would be to let _ stand for ImplicitP, which can become
>> either a dot pattern or a variable pattern (or a record pattern if issue
>> 473 is fixed).
>>
>> Cheers,
>> Andreas
>>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda