11

我正在读这个，我发现这个：

措施——为了让 Haskell 函数出现在细化类型中，我们需要将它们提升到细化类型级别。

还有其他文件声称需要采​​取措施才能在合同中使用此类功能。但我试过这个：

{-@ len :: List a -> Nat @-}
len :: List a -> Int
len Nil           = 0
len (x `Cons` xs) = 1 + len xs

{-@ mymap :: (a -> b) -> xs : List a -> { ys : List b | len xs == len ys } @-}
mymap :: (a -> b) -> List a -> List b
mymap _ Nil           = Nil
mymap f (x `Cons` xs) = f x `Cons` mymap f xs

这有效，但len不是衡量标准。那么究竟什么是测量值，什么时候需要呢？

另一个不工作的例子measure：

{-@ measure ln @-}
ln :: [a] -> Int
ln [] = 0
ln (x:y) = 1 + ln y

{-@ conc :: xs : [a] -> ys : [a] -> {zs : [a] | ln zs == ln xs + ln ys} @-}
conc :: [a] -> [a] -> [a]
conc [] ys = ys
conc (x:xs) ys = x : (conc xs ys)

我在许多文档中发现的 like 的使用{-@ measure length @-}会导致错误Cannot extract measure from haskell function（即 from length）。

4

1 回答 1

8

度量只是可以由 LiquidHaskell 在验证时运行的函数，用于细化和终止检查。您可能已经知道这一点。

您的第一个示例“有效”（我认为它按原样不完整，但我可以告诉您要做什么）的原因是它len已经被定义为LiquidHaskell 前奏曲中的一个度量（从技术上讲，它是一个“类度量”，这意味着它是多态的，因此可以与[]列表和您的自定义一起使用List）。假设您已经添加了注释，Nil并且Cons正如您之前问题的这个答案len中的那样，细化中使用的mymap不是 your len，而是 prelude len，这已经是一个措施。

在您的第二个示例中，measure是必需的，因为ln它是度量名称空间中的一个新符号，除非您创建它，否则它不存在。

于 2019-05-30T14:47:21.500 回答