合约 "true",使得 "assert true x==x" 成立

Contract "true", such that "assert true x==x" holds

是否可以编写一个检查声明是否真实的合约? 比如我要定义一个合约

true :: Contract a

对于所有值 x,等式

assert true x == x

持有。

我试过这样的方法:

true :: Contract a
true = Pred (\a -> True) 

但是当 运行ning assert true x == x 编译器说 x 是未定义的。 当运行宁assert true 5==6时,结果是False,而我希望得到一个Contract violation error。 我应该如何更改此 true 合同?非常感谢您的帮助。

这里

data Contract :: * -> * where
  Pred :: (a -> Bool) -> Contract a
  Fun  :: Contract a -> Contract b -> Contract (a -> b)

如果违反约定,断言将导致 运行 次失败,否则 return 原始结果:

assert :: Contract a -> a -> a
assert (Pred p)       x = if p x then x else error "contract violation"
assert (Fun pre post) f = assert post . f . assert pre

如果你考虑一下你对trueassert的定义,你会很清楚地看到问题。以下是相关部分:

true :: Contract a
true = Pred (\a -> True) 

assert :: Contract a -> a -> a
assert (Pred p)       x = if p x then x else error "contract violation"
...

将它们放在一起,您会看到 assert true x 将测试 (\a -> True) x 并产生 x 或抛出错误,具体取决于它是 True 还是 False.并且这将始终是 True,无论您对 x 使用什么表达式,因为根据定义谓词总是 returns True,并忽略其参数。

简单的解决方法是让 true "contract" 实际测试其参数,如下所示:

true :: Contract Bool
true = Pred id

也就是说,这个新的 true 只能应用于 Bool 类型的值(因为它对任何其他人都没有意义)并且对它没有任何作用。如果它是 True,它允许值不变,否则抛出你想要的违反合同的错误:

Prelude> assert true (5==6)
*** Exception: contract violation
CallStack (from HasCallStack):
  error, called at <interactive>:21:46 in interactive:Ghci2
Prelude> assert true (5==5)
True

并注意 assert true (5==6) 中的括号,因为 assert true 5==6 被解析为 (assert true 5)==6,因为函数应用程序是 Haskell 中最先例的 "operator" . assert true 5==6 导致错误,因为 true 的更正版本仅适用于布尔值,因此不适用于 5.

请注意,assert true x == xassert true xx 进行比较;所以 assert true 55 当然 5 == 6 是错误的,而不是违反合同。

如果您打算 assert true (x == x) 持有,那么

true :: Contract Bool
true = Pred id

assert true (5==6)  -- Contract violation

就是你想要的

"when running assert true x == x compiler says that x is undefined" 在这里相当关键。在我看来,您的 assert 调用是一个表达式,其中包含对 x 的两个引用,最外层的函数是 (==)。如果没有对 x 的绑定,任何一方都无法评估。 assert true x 部分永远不会出现 ==,如果我们将其重写为 assert true (x == x),我们仍然需要提供 x :: Eq a。我不知道如何检查这样的函数,但肯定有一些我不太熟悉的选项。