什么是度量？

Question

我正在阅读这个链接的内容，其中发现了以下信息：

Measures -- 为了允许 Haskell 函数出现在精化类型中，我们需要将它们提升到精化类型级别。

还有其他文件声称要使用这样的函数在合同中需要 measures 。但是我尝试了一下：

{-@ 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 @-}的使用方式，就像我在许多文档中发现的那样，会导致错误Cannot extract measure from haskell function（即从length中无法提取度量）。

- RandomB

---

声明长度为度量的正确语法是{-@ measure length :: Foldable t => t a -> Int @-}。看起来LH默认不会看到它的签名.. - RandomB

Answer 1

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

你第一个例子“有效”的原因（我认为它是不完整的，但我可以理解你的意思）是因为len已经被定义为一个LiquidHaskell prelude中的measure（技术上它是一个“class measure”，这意味着它是多态的，因此可以同时与[]列表和你的自定义List使用）。假设你已经按照你早前问题中的这个答案添加了Nil和Cons的注释，那么在mymap的细化中使用的len不是你的len，而是预定义的len，它已经是一个measure了。

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

- user11228628

---

哦，这很有道理，特别是预定义的 len。 - RandomB