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