LiquidHaskell：尝试使用 assume 关键字，但数据类型不是数字

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"

代码被判断为安全的，因为分母永远不会 returns 负值。

我觉得这很奇怪，因为我可以只写 x <= 0 作为后置条件，根据 Data.Ratio 模块的文档，这是不可能的。显然 Liquid Haskell 没有将我的后置条件与 denominator.

的实现进行比较

我的理解是，由于没有检查函数实现，所以我最好使用 assume 关键字：

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

我的问题是

LH 是不是应该强制我在这种情况下使用 assume 关键字，如果它显然没有通过与函数实现进行比较来验证我的细化类型的正确性？
我认为应该使用 assume 关键字是否正确？
为什么a突然不是数字了？我没用assume的时候不是数字吗？

Answer 1

不幸的是 'Numeric' 它的字面意思是 'Num' 而不是其子类。我们需要扩展 LH 以支持您上面描述的形式的 sub-类；我会为它创建一个问题，感谢您指出！

现在，如果您将类型专门化为，例如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 问题！

LiquidHaskell：尝试使用 assume 关键字，但数据类型不是数字

LiquidHaskell: Trying to use assume keyword, but data type is not numeric

haskell

liquid-haskell