haskell - LiquidHaskell : Trying to use assume keyword, 但数据类型不是数字

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 的文档模块是不可能的。显然 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  becauseThe sort a_a2kc is not numeric

我的问题是

1. LH 不应该强制我使用 assume在这种情况下，关键字是否显然没有通过与函数实现进行比较来验证我的精炼类型的正确性？
2. 我认为我应该使用 assume 对吗？关键字？
3. 怎么会a突然不是数字了？我没用assume的时候不就是数字吗？

Answer 1

不幸的是，“Numeric”的字面意思是“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

再次感谢您指出比率问题!