haskell - 如何在 Liquid Haskell 中编写 log2 函数

Question

我正在尝试从 book 学习 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)

但是在执行这段代码时出现了一些奇怪的错误，即“Refinement 中的排序错误”。我无法理解并解决此错误。

任何帮助将不胜感激。

编辑:来自 Liquid Haskell 书:

A Predicate is either an atomic predicate, obtained by comparing two expressions, or, an application of a predicate function to a list of arguments...

在 Liquid Haskell 逻辑语法中，允许的谓词之一是:e re e，其中 r 是原子二元关系(函数只是特殊类型的关系)。

此外，在教程中，他们将 Even 子类型定义为:{-@ type Even = {v:Int | v mod 2 == 0 } @-}

基于此，我认为 elem 应该可以工作。

但现在正如@ThomasM.DuBuisson 指出的那样，我想改为编写自己的elem'，以避免混淆。

elem' :: Int -> [Int] -> Bool
elem' _ [] = False
elem' e (x:xs)
 | e==x = True
 | otherwise = elem' e xs

现在，据我了解，为了能够使用此 elem' 作为谓词函数，我需要将其提升为度量。所以我添加了以下内容:

{-@ measure elem' :: Int -> [Int] -> Bool @-}

现在，我在 Powers 的类型定义中将 elem 替换为 elem'。但我仍然遇到与前一个相同的错误。

Answer 1

@TomMD 指的是“反射”的概念，它可以让您将 Haskell 函数(在某些限制下)转换为细化函数，例如请参阅这些帖子:

https://ucsd-progsys.github.io/liquidhaskell-blog/tags/reflection.html

不幸的是，尚未抽出时间使用此 Material 更新教程。

例如，您可以如下所示描述 log2/pow2:

https://ucsd-progsys.github.io/liquidhaskell-blog/tags/reflection.html

http://goto.ucsd.edu/liquid/index.html#?demo=permalink%2F1573673688_378.hs

特别是你可以写:

{-@ reflect log2 @-}
log2 :: Int -> Int
log2 1 = 0
log2 n = 1 + log2 (div n 2) 

{-@ reflect pow2 @-}
{-@ pow2 :: Nat -> Nat @-}
pow2 :: Int -> Int
pow2 0 = 1
pow2 n = 2 * pow2 (n-1)

然后您可以在编译时“检查”以下内容是否正确:

test8 :: () -> Int
test8 _ = log2 8 === 3

test16 :: () -> Int
test16 _ = log2 16 === 4

test3 :: () -> Int
test3 _ = pow2 3 === 8

test4 :: () -> Int
test4 _ = pow2 4 === 16 

但是，类型检查器将拒绝以下内容

test8' :: () -> Int
test8' _ = log2 8 === 5     -- type error

最后，可以证明以下有关log2和pow2的定理

{-@ thm_log_pow :: n:Nat -> { log2 (pow2 n) == n } @-}

“证明”是通过“n 归纳”，这意味着:

thm_log_pow :: Int -> () 
thm_log_pow 0 = ()
thm_log_pow n = thm_log_pow (n-1)

回到你原来的问题，你可以将 isPow2 定义为:

{-@ reflect isEven @-}
isEven :: Int -> Bool
isEven n = n `mod` 2 == 0

{-@ reflect isPow2 @-}
isPow2 :: Int -> Bool
isPow2 1 = True
isPow2 n = isEven n && isPow2 (n `div` 2) 

您可以通过验证以下内容来“测试”它是否做正确的事情:

testPow2_8 :: () -> Bool
testPow2_8 () = isPow2 8 === True 

testPow2_9 :: () -> Bool
testPow2_9 () = isPow2 9 === False 

最后，通过赋予 pow2 精炼类型:

{-@ reflect pow2 @-}
{-@ pow2 :: Nat -> {v:Nat | isPow2 v} @-}
pow2 :: Int -> Int
pow2 0 = 1
pow2 n = 2 * pow2 (n-1)

希望这有帮助!