Search code examples
haskellcontract

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

Is it possible to write a contract that checks whether a statement is true? For example, I want to define a contract

true :: Contract a

such that for all values x, the equation

assert true x == x

holds.

I have tried something like this:

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

But when running assert true x == x compiler says that x is undefined. When running assert true 5==6 the result is False, and I have hoped for a Contract violation error. How should I change this true contract? Would appreciate your help.

Here

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

Assert will cause a run-time failure if a contract is violated, and otherwise return the original result:

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
Solution

  • You can see the problem very clearly if you consider your definitions of true and assert. Here are the relevant parts:

    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"
...

    Put them together and you see that assert true x will test (\a -> True) x and either produce x or throw an error, depending on if it's True or False. And that this will always be True, no matter what expression you use for x, since the predicate by definition always returns True, and ignores its argument.

    The simple fix is to have the true "contract" actually test its argument, like this:

    true :: Contract Bool
true = Pred id

    That is, this new true can only apply to a value of type Bool (because it really doesn't make sense for any others) and does nothing to it. It lets the value through unchanged if it's True, and otherwise throws the contract violation error you want:

    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

    And note the parentheses in assert true (5==6), since assert true 5==6 is parsed as (assert true 5)==6, due to function application being the most precedent "operator" in Haskell. assert true 5==6 leads to an error because this corrected version of true only works on a Boolean value, and therefore not on 5.