-1

我正在阅读本教程，但我不确定我是否正确理解了文本（或者它是否完全正确）。有一个例子：

以下谓词是有效的，因为它们编码了前件推理方式：如果您知道 a 蕴含 b 并且您知道 a 为真，那么 b 也一定为真：

{-@ ex6 :: Bool -> Bool -> TRUE @-}
ex6 a b = (a && (a ==> b)) ==> b

{-@ ex7 :: Bool -> Bool -> TRUE @-}
ex7 a b = a ==> (a ==> b) ==> b

和 ex6 很好，但 ex7 不是，它失败了a = falseand b = false。LH 将其报告为：

Error: Liquid Type Mismatch

 88 | ex7 a b = a ==> (a ==> b) ==> b
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : GHC.Types.Bool | v <=> ((a => (a => b)) => b)}

   not a subtype of Required type
     VV : {VV : GHC.Types.Bool | VV}

   In Context
     a : GHC.Types.Bool

     b : GHC.Types.Bool

我也不明白他们对含义的定义：“你应该读 p ==> q 好像 p 是真的那么 q 也必须是真的”。它听起来不正确，因为它只断言一种情况：T -> T = T. 我在这里想念什么？可能是教程在“ex7”中有错误？

4

1 回答 1

4

我怀疑在示例中，他们已将其设为(==>)右关联，而在您的测试中，您将其保留为默认值，即左关联。比较：

> infixl 9 ==>; False ==> x = True; True ==> x = x
> False ==> (False ==> False) ==> False
False
> infixr 9 ==>; False ==> x = True; True ==> x = x
> False ==> (False ==> False) ==> False
True

该报告有更多细节。

于 2019-05-29T13:52:05.967 回答