LiquidHaskell：試圖用假設的關鍵字，但數據類型不是數字

Question

我嘗試寫一些規格的Data.Ratio模塊。到目前爲止，我有：

module spec Data.Ratio where 

import GHC.Real 

Data.Ratio.denominator :: GHC.Real.Integral a => r : GHC.Real.Ratio a -> {x:a | x > 0} 

我驗證的代碼是：

{-@ die :: {v:String | false} -> a @-} 
die msg = error msg 

main :: IO() 
main = do 
    let x = 3 % 5 
    print $ denominator x 
    if denominator x < 0 
    then die "bad ending" 
    else putStrLn "good ending" 

代碼判斷安全的，因爲分母永遠不會返回負值。

我發現這個很奇怪，因爲我可能剛剛寫了x <= 0作爲後置條件，根據Data.Ratio模塊的說明文檔是不可能的。顯然液體Haskell不會比較我的後置條件和denominator的實現。

我的理解是，由於未被選中的功能的實現，我最好使用假設關鍵字：

assume Data.Ratio.denominator :: GHC.Real.Integral a => r : GHC.Real.Ratio a -> {x:a | x > 0} 

不過，我再拿到：

 
Error: Bad Type Specification 
assumed type GHC.Real.denominator :: (Ratio a) -> {VV : a | VV > 0} 
    Sort Error in Refinement: {VV : a_a2kc | VV > 0} 
    Unbound Symbol a_a2kc 
Perhaps you meant: papp5, papp3, papp4, head, papp2, papp7, papp6, papp1, tail 
    because 
The sort a_a2kc is not numeric 

我的問題是

1. 不應該LH強迫我在這種情況下使用assume關鍵字如果它明顯didn'通過與函數實現進行比較來驗證我的精化類型的正確性？
2. 我是正確的思維，我應該用assume關鍵字？
3. 爲什麼a突然沒有數字？當我沒有使用assume時不是數字嗎？不幸的是

Answer 1

由「數字」它的字面意思是「民」，甚至不及其子類。我們需要擴展LH來支持上面描述的形式的子類;我會爲它創建一個問題，謝謝指出！現在

，如果你專注你的類型，例如如果你做的輸出類型x > 0那麼它是安全的再次

import GHC.Real 

{-@ assume denom :: r:GHC.Real.Ratio Int -> {x:Int | x >= 0} @-} 
denom :: GHC.Real.Ratio Int -> Int 
denom = denominator 

{-@ die :: {v:String | false} -> a @-} 
die msg = error msg 

main :: IO() 
main = do 
    let x = 3 % 5 
    print $ denom x 
    if denom x <= 0 
    then die "bad ending" 
    else putStrLn "good ending" 

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1504739852_3583.hs

：Int或Integer然後LH正確引發錯誤。

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1504739907_3585.hs

再次感謝您指出了Ratio問題！