LiquidHaskell: in mancanza di legge di DeMorgan

Question

Sto avendo difficoltà a comprovare il seguente legge con LiquidHaskell:

E 'noto come (uno dei) legge di DeMorgan, e semplicemente afferma che la negazione della or ing due valori deve essere uguale a and con la negazione di ciascuno. È stato dimostrato per molto tempo ed è un esempio in Liquidation tutorial di LiquidHaskell. Seguo lungo nel tutorial, ma non riescono a ottenere il seguente codice di passare:

-- 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) 

Quando si esegue liquid Test.hs, ottengo il seguente output:

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 

Ora sono in alcun modo un Esperto di LiquidHaskell, ma sono abbastanza sicuro che qualcosa deve essere sbagliato. Mi sono convinto che l'identità tiene a pochi anni fa, ma per assicurarsi che ho chiamato la funzione con ogni possibile ingresso, e, infine, corse

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

Quindi non mi sembra di avere un errore di battitura nel codice Haskell , l'errore deve trovarsi nella specifica LiquidHaskell. Sembra che LiquidHaskell non può dedurre che la risultante Bool è strettamente TRUE:

Inferred type 
    VV : Bool 

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

Qual è il mio errore qui? Qualsiasi aiuto è apprezzato!

PS: sto utilizzando il risolutore z3 ed eseguo GHC 7.10.3. La versione di LiquidHaskell è 2009-15.

Answer 1

LiquidHaskell non è in grado di dimostrare il proprio programma perché non ha un tipo sufficientemente potente per (<=>). Noi inferire tipi per funzioni, ma l'inferenza si basa sulle altre firme di tipo nel programma. Specificamente, è necessario capire che

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

(La sintassi Prop è come noi sollevare un Haskell Bool a un boolean SMT.)

Affinché per LiquidHaskell dedurre questo tipo, si dovrebbe vedere un predicato Prop v <=> (Prop p <=> Prop q) da qualche parte in un'altra firma di tipo (per alcuni v, p e q). Questo frammento non appare da nessuna parte, quindi dobbiamo fornire esplicitamente la firma.

È una sfortunata limitazione di LiquidHaskell, ma è fondamentale per mantenere la decidibilità.

PS: Ecco un collegamento a una versione funzionante del tuo esempio. http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1461434240_7574.hs