<div dir="ltr">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.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Jul 6, 2015 at 11:02 AM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Agda only case splits when there is a literal, constructor or absurd pattern. Variable and dot pattern do not induce splitting.<br>
<br>
Allowing _ to become a dot pattern would make it easier to explain hidden patterns, e.g. transH below could be said to simply mean<br>
<br>
transH {A = _}{a = _}{b = _}{c = _} refl refl = refl<br>
<br>
Currently, it is magic, meaning either of three things.<br>
<br>
Cheers,<br>
Andreas<div class="HOEnZb"><div class="h5"><br>
<br>
On 06.07.2015 10:33, Andrea Vezzosi wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
The need for "._" is certainly something that puzzles people learning<br>
Agda, this change would help for that.<br>
<br>
It makes "_" just a bit more special which might make it less<br>
intuitive in other ways, but as long as it's a backwards compatible<br>
change I think it's a good one.<br>
<br>
Do the dot patterns affect the generated case splitting tree?<br>
If so some proofs might break.<br>
<br>
Best,<br>
Andrea<br>
<br>
On Mon, Jul 6, 2015 at 10:25 AM, Andreas Abel <<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
P.S.: The standard library checks fine if one let _ stand for ImplicitP.<br>
<br>
<br>
On 06.07.2015 09:33, Andreas Abel wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
If you define transitivity of propositional equality without hiding<br>
value arguments, you have to explicitly choose where to put the dots:<br>
<br>
transV1 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c<br>
transV1 _ ._ ._ refl refl = refl<br>
<br>
transV2 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c<br>
transV2 ._ _ ._ refl refl = refl<br>
<br>
transV3 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c<br>
transV3 ._ ._ _ refl refl = refl<br>
<br>
With hidden arguments, you need not care:<br>
<br>
transH : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c<br>
transH refl refl = refl<br>
<br>
Of course, when giving the hidden arguments, it is the same as for<br>
visible arguments:<br>
<br>
transH1 : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c<br>
transH1 {a = _}{b = ._}{c = ._} refl refl = refl<br>
...<br>
<br>
The user has more flexibility when an argument is hidden. When an<br>
argument is given, the user has to actively make a decision whether a<br>
pattern must be a dot pattern or must not be one. There is no "I don't<br>
care, please figure it out for me" as there is for hidden arguments.<br>
This seems to be a mismatch.<br>
<br>
I think it would be simpler for the user if pattern "_" stood for "don't<br>
care" rather than "unnamed variable". The need for writing "._" would<br>
vanish.<br>
<br>
Does anything speak against this change? Is there a situation where it<br>
is essential to tell Agda not to let something be a dot pattern in order<br>
for type-checking to succeed? (In the end this could still be done by<br>
writing a named variable instead of _!)<br>
<br>
Internally, Agda has four kinds of trivial patterns:<br>
<br>
DotP ._ is (DotP MetaVariable)<br>
VarP x is (VarP "x") where x cannot be "_"<br>
WildP _ is WildP<br>
ImplicitP the user wrote no pattern (argument is hidden)<br>
<br>
The change would be to let _ stand for ImplicitP, which can become<br>
either a dot pattern or a variable pattern (or a record pattern if issue<br>
473 is fixed).<br>
<br>
Cheers,<br>
Andreas<br>
<br>
</blockquote>
<br>
<br>
--<br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" rel="noreferrer" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
</blockquote>
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" rel="noreferrer" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>