这些示例是否正确或教程有错误？

Question

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

The following predicates are valid because they encode modus ponens: if you know that a implies b and you know that a is true, then it must be the case that b is also true:

{-@ 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 = false 和 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

我也不明白他们对蕴涵的定义："You should read p ==> q as if p is true then q must also be true"。它听起来不正确，因为它只断言一种情况：T -> T = T。我在这里想念什么？教程可能在 "ex7"?

中有错误

Answer 1

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

> 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

Report 有更多详细信息。

这些示例是否正确或教程有错误？

Are these examples correct or the tutorial has an error?

haskell

liquid-haskell