haskell - 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 类型定义相同的函数。
对于文本类型，它出错了
例子

{-# 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 的一种奇特方式，所以我们原则上应该可以使用String推理 Text对象。所以我们引入一个措施来得到Text代表:

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

当我们构造一个 Text来自 String ，我们需要说 Text的表示是 String我们传入了(这编码了单射性， denot 扮演了相反的角色)。

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

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

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

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

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

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

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