Agda: what does `.(` mean?

Question

I was looking at the code in agda-stdlib/src/Data/Vec/Base.agda and saw .( in

take : ∀ m {n} → Vec A (m + n) → Vec A m
take m xs          with splitAt m xs
take m .(ys ++ zs) | (ys , zs , refl) = ys

I tried removing the . in front of it and got the following error:

Could not parse the left-hand side
take m (ys ++ zs) | (ys , zs , refl)
Operators used in the grammar:
  ++ (infixr operator, level 5) [_++_ (/Users/fss/Dropbox/Documents/projects/Coding/dev/agda/agda-stdlib/src/Data/Vec/Base.agda:99,1-5)]            
  ,  (infixr operator, level 4) [_,_ (/usr/local/Cellar/agda/2.6.1/share/x86_64-osx-ghc-8.10.1/Agda-2.6.1/lib/prim/Agda/Builtin/Sigma.agda:9,15-18)]
when scope checking the left-hand side
take m (ys ++ zs) | (ys , zs , refl) in the definition of take

So I'm guessing it is necessary. But I don't understand what it is for exactly. I tried to look in https://agda.readthedocs.io/en/v2.6.1.1 but couldn't find anything about it.

Thanks!

Answer 1

First off, in

take m (ys ++ zs) 

the pattern ys ++ zs is not valid because it is not a constructor applied on other patterns. If you think about it, in general it doesn't make sense to pattern match as function application because you'd need to be able to invert every function.

However, in

take : ∀ m {n} → Vec A (m + n) → Vec A m
take m xs          with splitAt m xs
take m .(ys ++ zs) | (ys , zs , refl) = ys

we pattern match on the result of splitAt as well. The type of the third argument is (ys ++ zs) == xs, and the type of the constructor refl is (ys ++ zs) == (ys ++ zs). By unification, that means xs ~ (ys ++ zs), so the second argument to take cannot be anything other than ys ++ zs in this clause.

And this is exactly what a dot-pattern means:

A dot pattern (also called inaccessible pattern) can be used when the only type-correct value of the argument is determined by the patterns given for the other arguments. The syntax for a dot pattern is .t.