4

我正在尝试为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"

代码被认为是安全的，因为 denominator 从不返回负值。

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

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

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

但是，我得到：

错误：错误的类型规范
 假定类型 GHC.Real.denominator :: (Ratio a) -> {VV : a | VV > 0}
     细化中的排序错误：{VV：a_a2kc | VV > 0}
     未绑定符号 a_a2kc
 也许你的意思是：papp5、papp3、papp4、head、papp2、papp7、papp6、papp1、tail
  因为
排序 a_a2kc 不是数字

我的问题是

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

1 回答 1

1

不幸的是，“数字”的字面意思是“数字”，甚至不是其子类。我们需要扩展 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问题！

于 2017-09-06T23:19:19.460 回答