7

问题

我对使用LiquidHaskell感到非常兴奋，但是，我不知道我需要在多大程度上修改我的原始 Haskell 代码才能满足 LiquidHaskell 的要求。

这是一个简单的示例，说明 Liquid 的规范如何适用于String类型，但不适用于Text类型。

对于 String 类型，它工作得很好

例子

我定义了一个 Liquid 类型，我们说元组的值不能相同：

{-@ type NoRouteToHimself = {v:(_, _) | (fst v) /= (snd v)} @-}

然后，对于String类型规范，它可以很好地工作，如下所示：

{-@ strOk :: NoRouteToHimself @-}
strOk :: (String, String)
strOk = ("AA", "AB")

LiquidHaskel 输出 >>结果：安全

{-@ strBad :: NoRouteToHimself @-}
strBad :: (String, String)
strBad = ("AA", "AA")

LiquidHaskel 输出 >>结果：不安全

到目前为止一切顺利，让我们为 Text 类型定义相同的函数。

对于文本类型，它出错了

例子

{-# LANGUAGE OverloadedStrings #-}
import qualified Data.Text as Tx

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo = ("AA", "AB")

预期结果： 结果：安全

LiquidHaskell 输出：结果：不安全

 ..Example.hs:102:3-5: Error: Liquid Type Mismatch
  
 102 |   foo = ("AA", "AB")
         ^^^
  
   Inferred type
     VV : {v : (Data.Text.Internal.Text, Data.Text.Internal.Text) | x_Tuple22 v == ?a
                                                                    && x_Tuple21 v == ?b
                                                                    && snd v == ?a
                                                                    && fst v == ?b}
  
   not a subtype of Required type
     VV : {VV : (Data.Text.Internal.Text, Data.Text.Internal.Text) | fst VV /= snd VV}
  
   In Context
     ?b : Data.Text.Internal.Text
      
     ?a : Data.Text.Internal.Text

显然 LiquidHaskell 无法评估这种情况下元组的值。有什么建议么？

4

2 回答 2

6

在玩了一些之后，我找到了一种方法可以做到这一点。我不知道保留 的多态性的方法NoRouteToHimself，但至少有一种方法可以谈论Data.Text对象的相等性。

该技术是引入一个外延度量。也就是说， aText实际上只是表示a的一种奇特方式String，因此我们原则上应该能够String对对象使用推理Text。所以我们引入了一个度量来获得Text代表什么：

{-@ measure denot :: Tx.Text -> String @-}

当我们Text从 a构造 a 时String，我们需要说Text' 表示是String我们传入的（这编码了单射性，denot扮演了逆的角色）。

{-@ assume fromStringL :: s:String -> { t:Tx.Text | denot t == s } @-}
fromStringL = Tx.pack

现在，当我们想比较TextLH 中不同 s 的相等性时，我们改为比较它们的外延。

{-@ type NoRouteToHimself = v:(_,_) : denot (fst v) /= denot (snd v) @-}

现在我们可以让示例通过：

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo = (fromStringL "AA", fromStringL "AB")

要使用Data.TextLH 中的其他函数，需要对这些函数给出指称规范。这是一些工作，但我认为这是值得做的事情。

我很好奇是否有办法使这种处理更具多态性和可重用性。我还想知道我们是否可以重载 LH 的平等概念，这样我们就不必经历denot. 有很多东西要学。

于 2019-02-05T00:36:01.670 回答
3

Liquid Haskell 通过利用原始 Haskell 构造函数来工作。String代码是糖

{-@ strOk :: NoRouteToHimself @-}
strOk :: (String, String)
strOk = (,) ('A':'A':[]) ('A':'B':[])

Liquid Haskell 知道如何解开/递归这些构造函数。但Data.Text不是根据 Haskell 构造函数定义的，而是使用不透明的转换函数——-XOverloadedStrings扩展插入它：

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo = (Tx.pack "AA", Tx.pack "AB")

在这里，Liquid Haskell 不知道它是如何Tx.pack工作的，它是否会在其输出中产生任何可解构的东西。一个也没有成功的更简单的例子是（没有-XOverloadedStrings）

{-@ foo :: NoRouteToHimself @-}
foo' :: (String, String)
foo' = (reverse "AA", reverse "AB")

为了完成这项工作，LH 至少需要知道这一点Tx.pack并且reverse是内射的。我对 LH 的了解还不够，无法判断是否有可能实现这一目标。也许强迫它内联转换函数就可以了。除此之外，唯一的选择是对值进行 NF 并调用==它的实际操作符——这在这种特殊情况下可以正常工作，但对于 LH 实际应该做的非平凡用例来说是不可能的。

于 2019-02-04T21:27:43.633 回答