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

[Ulf Norell]

I don't see any obvious problems with having _ mean ImplicitP. There might
be something to be said for being explicit about the fact that a visible
argument is dotted, but since it's clearly confusing people it's probably
better to change it.

/ Ulf

On Mon, Jul 6, 2015 at 11:02 AM, Andreas Abel <abela at chalmers.se> wrote:

> Agda only case splits when there is a literal, constructor or absurd
> pattern.  Variable and dot pattern do not induce splitting.
>
> Allowing _ to become a dot pattern would make it easier to explain hidden
> patterns, e.g. transH below could be said to simply mean
>
>   transH {A = _}{a = _}{b = _}{c = _} refl refl = refl
>
> Currently, it is magic, meaning either of three things.
>
> Cheers,
> Andreas
>
>
> On 06.07.2015 10:33, Andrea Vezzosi wrote:
>
>> 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
>>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
> --
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150706/934d3890/attachment.html