这是一个计算给定列表中数字平均值的简单函数。
{-@ 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 …根据我最近的问题，我一直在思考以下问题：
我们可以在LH中创建一些新的令人惊奇的类型，特别是表达一些整数的非平凡子集。例如：
{-@ type Nat = {v:Int | v>=0 } @-}
{-@ type grtN N = {v:Int | v>N } @-}
{-@ type Even = {v:Int | v mod 2 == 0 } @-}
但是，现在我可以在LH中表达什么其他非平凡的子集？
我可以在LH中创建仅包含2的幂的类型吗？这是我的最后一个问题，看来答案是否定的。
因此，一个自然的问题是我可以表达什么样的（整数）子集？有没有很好的特征？
为什么这会通过Liquid Haskell验证？
{-@ sub :: Nat -> Nat -> Int @-}
sub :: Int -> Int -> Int
sub i j = i - j
从LH的角度来看，这是否意味着Nat相同Int？
我正在尝试从书中学习 Liquid Haskell 。为了测试我的理解，我想编写一个函数log2，它接受形式为 2^n 的输入并输出 n。
我有以下代码：
powers :: [Int]
powers = map (2^) [0..]
{-@ type Powers = {v:Nat | v elem powers } @-}
{-@ log2 :: Powers -> Nat @-}
log2 :: Int -> Int
log2 n
| n == 1 = 0
| otherwise = 1 + log2 (div n 2)
但是在执行这段代码时出现了一些奇怪的错误，即“Sort Error in Refinement”。我无法理解和解决此错误。
任何帮助将非常感激。
编辑：从 Liquid Haskell 书中：
谓词要么是原子谓词，通过比较两个表达式获得，要么是谓词函数对参数列表的应用......
在 Liquid Haskell 逻辑语法中，允许的谓词之一是：e r ewherer是原子二元关系（而函数只是一种特殊的关系）。 …