LiquidHaskell:DeMorgan法律失败

Question

我在使用LiquidHaskell证明以下法律时遇到了麻烦:

它被称为DeMorgan定律(之一),并简单地指出,or对两个值的否定必须and与每个值的否定相同.它已经被证明了很长时间,并且是LiquidHaskell 教程中的一个例子.我正在学习本教程,但未能通过以下代码:

-- 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).此片段不会出现在任何地方,因此我们需要明确提供签名.

这是LiquidHaskell的一个不幸的限制,但对于保持可判定性至关重要.

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