[Agda] question on `Any'

[Dominique Devriese]

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