阿格达：`.(` 是什么意思？

Question

我正在查看 agda-stdlib/src/Data/Vec/Base.agda 中的代码并在

中看到 .(

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

我尝试删除它前面的 . 并得到以下错误：

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

所以我猜这是必要的。但我不明白它到底是干什么用的。我试图查看 https://agda.readthedocs.io/en/v2.6.1.1 但找不到任何相关信息。

谢谢！

Answer 1

首先，在

take m (ys ++ zs)

模式 ys ++ zs 无效，因为它不是应用于其他模式的构造函数。如果您考虑一下，通常将模式匹配作为函数应用程序没有意义，因为您需要能够反转每个函数。

然而，在

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

我们也对 splitAt 的结果进行模式匹配。第三个参数的类型是(ys ++ zs) == xs，构造函数refl的类型是(ys ++ zs) == (ys ++ zs)。通过统一，这意味着 xs ~ (ys ++ zs)，因此 take 的第二个参数不能是此子句中 ys ++ zs 以外的任何内容。

这正是 dot-pattern 的意思：

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.

阿格达：`.(` 是什么意思？

Agda: what does `.(` mean?

syntax

pattern-matching

unification

agda