LiquidHaskell 在“Data.String”类型上运行良好但在“Data.Text”类型上运行良好的简单案例

Question

问题

我对使用 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 类型定义相同的函数。

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 在这种情况下无法评估元组的值。有什么建议吗？

Answer 1

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

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

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

当我们从String构造Text时，我们需要说Text的外延是我们传入的String（这编码了注入性，denot扮演了逆）。

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

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

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

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

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

要在 LH 中使用 Data.Text 的其他功能，需要为这些功能提供指称规范。这是一些工作，但我认为这是值得做的事情。

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

Answer 2

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 实际应该使用的非平凡用例来说是不可能的做。