Жидкий haskell создает новую бистринг с PS - PullRequest
Новая
       27

Жидкий haskell создает новую бистринг с PS

0 голосов
/ 30 ноября 2018

Я делаю некоторые привязки к C из Haskell и пытаюсь сделать его более безопасным с помощью LiquidHaskell.У меня возникли проблемы с указанием длины строки байтов в аннотации типа LH.

У меня есть расширенный тип ByteString в LiquidHaskell, который включает его длину: 

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

1 Ответ

0 голосов
/ 30 мая 2019

LiquidHaskell не знает, что ByteString, возвращаемое makeBs, имеет длину l, и не может доказать это из имеющейся у него информации.

Вы знаете, что это произойдет, потому что выЗнайте, что третий аргумент конструктора PS - это длина.Таким образом, на данный момент у вас есть два (или, возможно, один) варианта:

  1. Вы можете попытаться рассказать LH, что вы знаете о конструкторе PS, и дать ему аннотацию типа {-@ Bi.PS :: _ -> _ -> l:NonNeg -> ByteString l @-}.Я попробовал это, и это не совсем сработало, потому что в сигнатуре PS есть внутренние типы GHC, с которыми LH не справляется.YMMV.Или вы можете:
  2. Забудьте об аннотировании PS и пометьте свою собственную функцию с помощью assume: {-@ assume makeBs :: ForeignPtr Word8 -> l:NonNeg -> ByteString l @-}.Конечно, это становится более рискованным, если функция, помеченная assume, становится больше - глупо, хотя это может показаться, что вы, возможно, захотите сохранить makeBs, если будете идти по этому пути.
...