[Agda] question on `Any'
Dominique Devriese
dominique.devriese at cs.kuleuven.be
Sun Aug 18 18:51:13 CEST 2013
Sergei,
2013/8/18 Sergei Meshveliani <mechvel at botik.ru>:
> On Tue, 2013-08-13 at 14:34 +0200, Dominique Devriese wrote:
>> Try changing the following line
>>
>> > f x _ (here _) = []
>>
>> to use a dot pattern
>>
>> f x ._ (here _) = []
>>
>> For more info, see the Agda tutorial by Norell and Chapman for
>> example. They mention the following rule:
>> The rule for when an argument should be dotted is: if there is a unique
>> type correct value for the argument it should be dotted.
>>
>> In this case, the value of the underscore is fixed by the type of (here _).
> 1) ``should be dotted'' or ``must be dotted'' ?
Indeed, "must be dotted".
> 2) > the value of the underscore is fixed by the type of (here _)
>
> But it is not fixed.
> If x ≈ a, x ≈ b, then the value for the first underscore in the line
> can be, say,
> a :: [], b :: a :: c :: [], ...
Take into account implicit arguments. The type of here is:
here : ∀ {x xs} (px : P x) → Any P (x ∷ xs)
and the type of f is:
f : (x : C) → (ys : List C) → Any (_≈_ x) ys → List C
Then the following line
f x ._ (here _) = []
actually means
f x ._ (here {x} {xs} _) []
and the type of "here _" is "Any (_≈_ x) (x' :: xs)"
Given "f"'s type, this implies that the dotted argument must be equal
(exactly) to "x' :: xs".
> The pattern .(_ :: _)
>
> probably, tells ``some non-empty list over C'',
> it looks sensible, and it is checked.
Yes, this works too.
Another alternative is making the dotted pattern fully precise (:
f x .(x' :: xs) (here {x} {xs} _) []
> But what does this mean here `._'
> -- this is a question.
> The fact that it is type-checked looks strange.
I'm not aware of a precise definition of _ in a dotted pattern
anywhere. I read "._" as "some expression that is implied by the
type of the rest of the LHS".
Regards
Dominique
More information about the Agda
mailing list