时间戳

首页 > 解决方案 > Liquid haskell 用 PS 创建一个新的字节串

haskell - Liquid haskell 用 PS 创建一个新的字节串

问题描述

我正在从 Haskell 对 C 进行一些绑定，并尝试使用 LiquidHaskell 使其更安全。我在指定 LH 类型注释中的字节串长度时遇到了一些麻烦。

我在 LiquidHaskell 中有一个增强的 ByteString 类型，包括它的长度：

{-@ type ByteString Blen = {v:B.ByteString | bslen v == Blen} @-}

运行 Liquidhaskell 时出现以下错误：

**** RESULT: UNSAFE ************************************************************


 /home/t/liquidproblem/Main.hs:47:3-22: Error: Liquid Type Mismatch

 47 |   Bi.PS foreignPtr 0 l
        ^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : Data.ByteString.Internal.ByteString | 0 <= bslen v
                                                     && bslen v == stringlen v}

   not a subtype of Required type
     VV : {VV : Data.ByteString.Internal.ByteString | bslen VV == l}

   In Context
     l : {l : GHC.Types.Int | l >= 0}

第 47 行是：

44 {-@ makeBs :: ForeignPtr Word8 -> l:NonNeg -> ByteString l @-}
45 makeBs :: F.ForeignPtr F.Word8 -> Int -> B.ByteString
46 makeBs foreignPtr l =
47   Bi.PS foreignPtr 0 l

（我知道这似乎是一个愚蠢的功能，但它被放入是因为调试过程是为了分解位并将 LH 注释放在它们上，直到我发现问题为止。）

相关的进口是：

import qualified Data.ByteString.Internal as Bi
import qualified Data.ByteString as B
import qualified Foreign as F

LH NonNeg 类型是

{-@ type NonNeg = {i:Int | i >= 0} @-}

标签： haskellliquid-haskell

解决方案

LiquidHaskell 不知道ByteString返回的makeBs有 length l，并且无法从可用的信息中证明这一点。

你知道它会，因为你知道PS构造函数的第三个参数是长度。因此，此时您有两个（或可能一个）选项：

  1. 您可以尝试告诉 LH 您对PS构造函数的了解，并给它一个注释，例如 {-@ Bi.PS :: _ -> _ -> l:NonNeg -> ByteString l @-}. 我试过了，但效果不太好，因为 LH 的签名中有内部 GHC 类型PS似乎不太擅长处理。YMMV。或者，您可以：
  2. 忘记注释并使用:PS标记您自己的函数。当然，如果标有 的函数变得更大，这会变得更加冒险——尽管看起来很愚蠢，但如果你走这条路，你可能想保留。assume{-@ assume makeBs :: ForeignPtr Word8 -> l:NonNeg -> ByteString l @-}assumemakeBs

推荐阅读