继任者上的 Idris 模式匹配（下一个值）答案

【问题标题】：Idris pattern matching on successor (next value)继任者上的 Idris 模式匹配（下一个值）
【发布时间】：2020-07-15 10:13:02
【问题描述】：

在下面的函数中，我在 (S k) 上的 k 的后继上进行模式匹配

vectTake : (n : Nat) -> Vect (n + m) a -> Vect n a
vectTake Z xs = []
vectTake (S k) (x :: xs) = x :: vectTake k xs

如果需要，是否可以在函数体上使用该值？

另一种解决方案是在 k 上匹配并在 body 函数上使用 k 的前身，这样解决同一问题的另一种形式或这种模式匹配提供了我看不到的任何其他优势？

【问题讨论】：

我不确定你的意思。您已经在使用k，如果您稍微更改签名（和功能），您可以使用S k ... vectTake (S k) (x :: xs) = (S k) :: vectTake k xs
也许你的意思是命名模式vectTake count@(S k) (x :: xs) = count :: vectTake k xs
@JoelB 感谢您的回答，当我问“是否可以在需要时在函数体上使用该值？”时，他们都解决了我的意思。太好了，你让我想起了命名功能让我试着更好地解释第二个问题，我们可以这样做：vectTake k (x :: xs) = x :: vectTake (pred k) xs 吗？如果是，(S k) 中的模式匹配比 k 有什么优势？ ——

【解决方案1】：

关于你的第一个问题...

Nat 的（原始）定义是

data Nat = Z | S Nat

我们可以匹配：

一旦你匹配了一个值，你就可以做你通常可以用Nat做的所有事情，包括使用S构造后继，所以如果你想匹配S k并使用它一个函数，你可以

...
vectTake (S k) (x :: xs) = (S k) :: vectTake k xs

虽然在这里我改变了你的功能的含义来说明我的观点。在此示例中，您还可以使用 命名模式

...
vectTake count@(S k) (x :: xs) = count :: vectTake k xs

关于你的第二个问题...

pred k 我假设您的意思是前任而不是谓词。如果是这样，你可以对Nat进行整数运算，包括k - 1，所以，回到vecTake的原始定义

...
vectTake k (x :: xs) = x :: vectTake (k - 1) xs

请注意，这依赖于 Z 的匹配首先出现，否则您最终会执行 Z - 1，这将无法编译。

至于在Z 和S k 或Z 和k 上匹配哪个更好，我想不出任何客观原因说明一个人比另一个人更好。也许在某些情况下会涉及到性能，但我无法帮助你。我主要使用构造函数模式，因为人们会习惯于看到这一点，但我确信在某些情况下需要其他样式。

【讨论】：