在 Liquid 中定义度量 Haskell

Question

这是一个计算给定列表中数字平均值的简单函数。

{-@ type NonZero = {v:Int | v/=0 } @-}

{-@ divide :: Int -> NonZero -> Int @-}
divide :: Int -> Int -> Int
divide n d = div n d

{-@ measure nonEmpty :: [a] -> Bool @-}
nonEmpty [] = False
nonEmpty _ = True

{-@ size :: xs:[a] -> {v:Nat | nonEmpty xs => v>0 } @-}
size :: [a] -> Int
size [] = 0
size (_:xs) = 1 + size xs

{-@ type NEList a = {v:[a] | nonEmpty v} @-}

{-@ avg :: NEList Int -> Int @-}
avg xs = divide (sum xs) (size xs)

遗憾的是这段代码没有类型检查。

但是如果我在定义函数后声明 nonEmpty 是一个度量，它会起作用：

{-@ type NonZero = {v:Int | v/=0 } @-}

{-@ divide :: Int -> NonZero -> Int @-}
divide :: Int -> Int -> Int
divide n d = div n d

{-@ nonEmpty :: [a] -> Bool @-}
nonEmpty [] = False
nonEmpty _ = True
{-@ measure nonEmpty @-}

{-@ size :: xs:[a] -> {v:Nat | nonEmpty xs => v>0 } @-}
size :: [a] -> Int
size [] = 0
size (_:xs) = 1 + size xs

{-@ type NEList a = {v:[a] | nonEmpty v} @-}

{-@ avg :: NEList Int -> Int @-}
avg xs = divide (sum xs) (size xs)

那么有人可以解释为什么会这样吗？

Answer 1

这是因为 LH 希望通过第二种语法（而不是第一种）来声明度量。然而，不幸的是，LH 目前不会给出第一个错误消息，它似乎只是默默地忽略度量定义（或者更确切地说，将其视为 "uninterpreted"）。

我们将修复代码，以便在有实际定义时告诉您。

简而言之：这是我们语法选择的不幸结果，我深表歉意！

在 Liquid 中定义度量 Haskell

Defining measures in Liquid Haskell

haskell

liquid-haskell