如何解决检查功能应用程序是不可能的?
我想检查我的函数签名的含义,我认为它们的含义。我当然可以检查阳性变异
test_concat : Vect [3] Nat -> Vect [2] Nat -> Vect [5] Nat
test_concat x y = x ++ y
但我想测试一些负面的变体,比如
test_concat_invalid : Vect [3] Nat -> Vect [2] Nat -> Vect [1] Nat -> Void
test_concat_invalid x y = x ++ y impossible
虽然显然语法是组成的。我发现我可以做一些类似于测试的事情,如果我正确地编写了一个用于证明的数据构造函数。这可能吗?
解决方法
您可以创建一个由单独的类型和值索引的类型:
data Typed : Type -> a -> Type where
MkTyped : {A : Type} -> {x : A} -> Typed A x
但只提供一个将类型索引与值索引联系起来的构造函数——即只有当值 Typed
的类型为 x
时才能构造 A
。
这让我们可以这样写一个命题:
test_concat_invalid
: (x : Vect 3 Nat)
-> (y : Vect 2 Nat)
-> Typed (Vect 1 Nat) (x ++ y)
-> Void
test_concat_invalid _ _ MkTyped impossible
当 Idris 尝试统一类型时,通过构造,它看到 1 不是 5,它们明显不同。这意味着 Idris 会很乐意接受 MkTyped
构造函数在这个命题中是不可能的。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。