契约“ true”，使得“ assert true x == x”成立

Question

是否可以写一份合同来检查陈述是否正确？例如，我想定义一个合同

true :: Contract a

这样对于所有值x，方程

assert true x == x

持有。

我已经尝试过这样的事情：

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

但是在运行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)

如果违反合同，则声明将导致运行时失败，否则将返回原始结果：

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

Answer 1

你可以很清楚地看到这个问题，如果你认为你的定义true和assert。以下是相关部分：

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因为按定义，谓词始终返回True，而忽略其参数。

一个简单的解决方法是让true“合同”实际测试其参数，如下所示：

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

并请注意，由于函数应用程序是Haskell中最先例的“运算符”，因此括号中的assert true (5==6)，由于assert true 5==6被解析为(assert true 5)==6，因此括号中为。assert true 5==6导致错误，因为的更正版本true仅适用于布尔值，因此不适用于5。