什么措施？

Question

我读这个，我觉得这样的：

措施 -为了使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)

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

Answer 1

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

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

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