如何验证不符合预期的函数签名应用是不可能实现的？

这种针对函数签名的负向验证在支持依赖类型和命题否定的语言（如Idris、Agda、Coq）中完全可以实现，核心逻辑是利用命题否定的标准定义：Not P = P -> Void，即只要证明「不符合预期的情况成立会推导出荒谬（Void类型的值）」，即可完成负向验证。

以Idris为例的实现方案 #

你要验证的「长度为3的Nat向量和长度为2的Nat向量拼接，不可能得到长度为1的Nat向量」，可以直接用Idris原生的impossible关键字实现，代码如下：

import Data.Vect
import Data.Nat

-- 负向测试用例：若传入x ++ y = z的相等证明，可推导出荒谬
test_concat_invalid : (x : Vect 3 Nat) -> (y : Vect 2 Nat) -> (z : Vect 1 Nat) -> (x ++ y = z) -> Void
test_concat_invalid [] _ _ Refl impossible
test_concat_invalid (_::_) _ _ Refl impossible

上述代码中，Refl是Idris中命题相等的唯一构造子，当匹配到Refl时意味着编译器需要同时满足3 + 2 = 5和5 = 1，显然不可能，因此两个分支都被标记为impossible。只要这段代码能正常编译通过，就说明你需要的负向约束成立。

如果希望更贴近你给出的伪代码写法，也可以通过标准库的absurd函数简化写法，不用显式传入相等证明：

test_concat_invalid_simple : Vect 3 Nat -> Vect 2 Nat -> Vect 1 Nat -> Void
test_concat_invalid_simple x y z = absurd $ the (x ++ y = z) %search

其他场景说明 #

• Agda中可以使用()荒谬模式标记不可能出现的模式分支，逻辑和Idris完全一致
• Coq中可以通过inversion、contradiction等策略推导矛盾完成证明
• 无依赖类型支持的普通静态类型语言（如Haskell、Rust）无法直接实现这类和值属性绑定的签名负向验证，只能通过运行时测试、类型级编程hack实现有限的校验效果

内容的提问来源于stack exchange，提问作者joel