haskell - 什么是度量？

Question

我正在阅读 this我在哪里找到这个:

Measures -- In order to allow Haskell functions to appear in refinement types, we need to lift them to the refinement type level.

还有其他文件声称需要采​​取措施才能在契约(Contract)中使用此类功能。但我试过这个:

{-@ 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 )。

Answer 1

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

您的第一个示例“有效”的原因(我认为它按原样不完整，但我可以告诉您您的目的)是 len已定义为度量 in the LiquidHaskell prelude (从技术上讲，它是一个“类度量”，这意味着它是多态的，因此可以与 [] 列表和您的自定义 List 一起使用)。假设您已为 Nil 添加注释和 Cons如 this answer从您之前的问题中，len用于 mymap 的细化不是你的len ，但前奏len ，这已经是一个措施。

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