问题描述
我正在查看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,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,refl) in the deFinition of take
所以我想这是必要的。但是我不明白这到底是什么。我试图查看https://agda.readthedocs.io/en/v2.6.1.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的意思:
当参数的唯一类型正确值由为其他参数指定的模式确定时,可以使用点模式(也称为不可访问模式)。点图案的语法为
.t
。