[Agda] Should not _ patterns be resolvable by inaccessible
patterns?
Andreas Abel
abela at chalmers.se
Mon Jul 6 11:02:22 CEST 2015
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/
More information about the Agda
mailing list