5

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

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

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

4

1 回答 1

4

这是因为 LH 期望通过第二种语法（而不是第一种）声明度量。然而，不幸的是，LH 目前没有给出第一个错误消息，它似乎只是默默地忽略了度量定义（或者更确切地说，将其视为“未解释的”）。

我们将修复代码，以便当有实际定义时，它会告诉您有关它的信息。

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

于 2019-11-14T01:12:28.597 回答