LiquidHaskell：没有，我有麻烦证明下列法律与LiquidHaskell德·摩根定律

：LiquidHaskell：没有，我有麻烦证明下列法律与LiquidHaskell德·摩根定律

这是被称为（之一）德·摩根定律，并简单地指出的or否定荷兰国际集团的两个值必须与每个的否定相同。它已被证明很长一段时间，并且是LiquidHaskell's 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 

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

{[email protected] 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。

来源

2016-04-23 Nicolas Mattia

我想知道，也许这是一个更合适的液体哈斯克尔问题。但是，这些可能是目前在stackoverflow上可用的最近的标签。 –

不幸的是，没有液体哈斯克尔标签，我需要更多的声望来创建一个。我希望那些传达这个想法。 –

dfeuer：感谢您的标签！ –

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

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

（该Prop语法是我们如何解除哈斯克尔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

来源

2016-04-23 18:05:40

事实上，有一条线缺失：'{ - @（<=>）:: p：Bool - > q：Bool - > {v：Bool | Prop v <=>（Prop p <=> Prop q）} @ - } '。我认为这是LiquidHaskell的默认设置。现在让我想起这样的初级功能也是由用户定义的，几乎与Haskell大多数情况一样，“关键字”实际上不是关键字。感谢你的回答！ –

我是唯一一个在点击http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1461434240_7574.hs上的“检查”按钮时发生错误的人吗？ –

LiquidHaskell：没有，我有麻烦证明下列法律与LiquidHaskell德·摩根定律

回答

相关问题