1

我正在关注 Liquid Haskell 教程：

http://ucsd-progsys.github.io/liquidhaskell-tutorial/04-poly.html

这个例子失败了：

module Test2 where

import Data.Vector
import Prelude hiding (length)

vectorSum :: Vector Int -> Int
vectorSum vec = go 0 0
  where
    go acc i
      | i < length vec  = go (acc + (vec ! i)) (i + 1)
      | otherwise       = acc

出现以下错误：

Error: Liquid Type Mismatch

 10 |       | i < length vec  = go (acc + (vec ! i)) (i + 1)
                                   ^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : GHC.Types.Int | v == acc + ?b}

   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV < acc
                                && VV >= 0}

   In Context
     ?b : GHC.Types.Int
     acc : GHC.Types.Int

问题是为什么？守卫 (i < length vec) 应该确保 (vec ! i) 是安全的。

4

2 回答 2

0

首先，我不知道您使用的是哪个版本的 LH，但我遇到了完全相同的问题。该教程指出

LiquidHaskell 验证 vectorSum ——或者，准确地说，访问 vec 的向量的安全性！一世。验证成功是因为 LiquidHaskell 能够自动推断

go :: Int -> {v:Int | 0 <= v && v <= sz} -> Int

它表明第二个参数 i 介于 0 和 vec 的长度（含）之间。LiquidHaskell 使用这个和 i < sz 的测试来确定 i 在 0 和 (vlen vec) 之间来证明安全性。

他们还声明本教程不符合 LiquidHaskell 的当前版本。

自编写教程以来，LH 的（细化）类型推断似乎发生了一些变化，可能比以前更泛化了类型，从而导致了这个问题。

问题不在于 LH 没有正确识别后卫。问题是它无法验证属性0 <= v。

以下检查适用于 LH 0.8.6.2 版：

{-@ LIQUID "--short-names"         @-}
{-@ LIQUID "--no-termination"      @-}
{-@ LIQUID "--reflection"          @-}

import Prelude hiding (length)
import Data.Vector 

{-@ go' :: v:Vector Int -> Int -> {i:Int | i>=0 } ->Int @-}
go' :: Vector Int -> Int -> Int -> Int
go' vec acc i
    | i < sz    = go' vec (acc + (vec ! i)) (i + 1)
    | otherwise = acc
    where sz = length vec

vecSum :: Vector Int -> Int
vecSum vec = go' vec 0 0

似乎 LH 推断出 go 本身就是一个函数，并且可以用小于 0 的整数调用（显然不是）。

我仍然在玩这个例子来说服 LH 这个事实。如果有人在这方面取得了更大的成功，请发表评论。

编辑：

我在同一个教程中找到了以下段落；似乎这可能已经改变：

在调用loop 0 n 0 body时，参数lo和分别用和hi实例化，顺便说一下，这是推理引擎推断非负性的地方。0n

于 2020-03-28T13:11:18.420 回答
0

这看起来像一个终止错误。Liquid Haskell 这里似乎假设这acc是go（可能是因为它是第一个Int参数）的终止指标。因此，它应该始终是非负的并且在每次迭代中都会减少（因此您会收到错误消息）。

解决这个问题的方法是提供一个正确的终止指标，它满足上述标准。这将是length vec - i，相应的签名go是：

{-@ go :: _ -> i:_ -> _ /[length vec - i] @-}

或类似的规定。

于 2022-03-02T14:10:44.113 回答