LiquidHaskell：assumキーワードを使用しようとしましたが、データ型が数値ではありません

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をポストコンディションとして書いたことがあるので、これは奇妙です。明らかにLiquid 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ではキーワードを使用しないようにしてください。関数の実装と比較して洗練された型の正確性を検証しますか？
2. 私はassumeキーワードを使うべきだと思っていますか？
3. どうしてaが突然数値ではないのですか？私がassumeを使用しなかったときに数値ではなかったか？

Answer 1

残念なことに「数値」は文字通り「Num」を意味し、そのサブクラスも意味しません。上記で説明した形式でサブクラスをサポートするには、LHを拡張する必要があります。私は指摘のおかげでそれのための問題を作成します！

ここで、あなたのタイプを例えばに特化すれば、 IntまたはIntegerその後、LHは正常にエラーがスローされます：

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

あなたは、出力タイプx > 0を作るならば、それは再び安全です。

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

おかげで再びRatio問題を指摘して！