LiquidHaskell：不符合德摩根定律

Question

我无法用 LiquidHaskell 证明以下定律：

它被称为 DeMorgan 定律（之一），它简单地指出 or 两个值的否定必须与 and 对每个值的否定相同。它已经被证明了很长时间，并且是 LiquidHaskell 的 tutorial 中的一个例子。我正在按照教程进行操作，但未能通过以下代码：

-- Test.hs
module Main where

main :: IO ()
main = return ()

(==>) :: Bool -> Bool -> Bool
False ==> False = True
False ==> True  = True
True  ==> True  = True
True  ==> False = False

(<=>)  :: Bool -> Bool -> Bool
False <=> False = True
False <=> True  = False
True  <=> True  = True
True  <=> False = False

{-@ type TRUE  = {v:Bool | Prop v}       @-}
{-@ type FALSE = {v:Bool | not (Prop v)} @-}

{-@ deMorgan :: Bool -> Bool -> TRUE @-}
deMorgan :: Bool -> Bool -> Bool
deMorgan a b = not (a || b) <=> (not a && not b)

当运行 liquid Test.hs时，我得到以下输出：

LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.


**** DONE:  Parsed All Specifications ******************************************


**** DONE:  Loaded Targets *****************************************************


**** DONE:  Extracted Core using GHC *******************************************

Working   0%     [.................................................................]
Done solving.

**** DONE:  solve **************************************************************


**** DONE:  annotate ***********************************************************


**** RESULT: UNSAFE ************************************************************


 Test.hs:23:16-48: Error: Liquid Type Mismatch

 23 | deMorgan a b = not (a || b) <=> (not a && not b)
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : Bool

   not a subtype of Required type
     VV : {VV : Bool | Prop VV}

   In Context

现在我绝不是 LiquidHaskell 专家，但我很确定一定有问题。几年前我就说服自己这个身份成立，但为了确保我用每一个可能的输入调用了这个函数，最终运行

λ: :l Test.hs 
λ: import Test.QuickCheck
λ: quickCheck deMorgan 
>>> +++ OK, passed 100 tests.

所以我似乎没有在Haskell代码中输入错误，错误必须出在LiquidHaskell规范中。似乎 LiquidHaskell 无法推断结果 Bool 是严格的 TRUE:

Inferred type
  VV : Bool

not a subtype of Required type
  VV : {VV : Bool | Prop VV}

我这里的错误是什么？任何帮助表示赞赏！

PS：我正在使用 z3 求解器和运行 GHC 7.10.3。 LiquidHaskell 版本是 2009-15.

Answer 1

LiquidHaskell 无法证明您的程序安全，因为它没有足够强的类型供 (<=>) 使用。我们确实为函数推断类型，但推断是基于程序中的其他类型签名。具体来说，我们需要弄清楚

{-@ (<=>) :: p:Bool -> q:Bool -> {v:Bool | Prop v <=> (Prop p <=> Prop q)} @-}

（Prop 语法是我们将 Haskell Bool 提升为 SMT 布尔值的方式。）

为了让 LiquidHaskell 推断出这种类型，它需要在另一个类型签名的某处看到谓词 Prop v <=> (Prop p <=> Prop q)（对于某些 v、p，以及 q）。此片段未出现在任何地方，因此我们需要明确提供签名。

这是 Liquid 的一个不幸限制Haskell，但对于保持可判定性至关重要。

PS：这是您示例的工作版本的 link。 http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1461434240_7574.hs

LiquidHaskell：不符合德摩根定律

LiquidHaskell: failing DeMorgan's law

haskell

z3

boolean-logic

liquid-haskell