我写了一些代码在 Haskell 中进行序数运算，现在我正在尝试使用 Liquid Haskell 来验证某些属性。但是，我在“反映”递归函数时遇到了麻烦。我在下面的“小于”函数中发现了一个问题：

liquid ordinals.hs仅使用上述执行会产生以下错误：

那么反映递归函数的正确方法是什么？我已经阅读了液体 haskell 教程，但我无法弄清楚它的示例有什么不同。

作为我遇到的问题的一个最小示例，这里有一个自然数的定义、一个加倍函数和一个由偶数谓词细化的类型：

我想先声明{-@ double' :: Nat' -> Even' @-}然后证明这是真的，但我的印象是我必须先写证明然后使用castWithTheorem（它本身对我有用）这样：

但是，这会产生相当难以辨认的错误，例如：

我究竟做错了什么？从我的实验来看，这似乎是由于试图证明某些谓词函数对某些论点是正确的。

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

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

运行 Liquidhaskell 时出现以下错误：

第 47 行是：

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

相关的进口是：

LH NonNeg 类型是

我最近一直在玩 LiquidHaskell 和 Idris，我有一个非常具体的问题，我无法在任何地方找到明确的答案。

Idris 是一种依赖类型的语言，在大多数情况下都很棒。但是我读到类型检查期间的某些类型术语可能会从编译时“泄漏”到运行时，即使是强硬的 Idris 也会尽力消除这些术语（这甚至是一个特殊功能......）。但是，这种消除并不完美，有时确实会发生。如果、为什么以及何时发生这种情况并不能从代码中立即清楚地看到，并且有时会对运行时性能产生影响。

我见过人们更喜欢 Haskells 的类型系统，因为它不可能在那里发生。当类型检查完成时，它就完成了。类型被“丢弃”并且在运行时不使用。

LiquidHaskell 的故事是什么？与传统的 Haskell 相比，它大大增强了类型系统的功能。LiquidHaskell 是否还为某些类型的“星座”注入运行时位，或者（我怀疑）只是在 Haskell 上添加另一层“更好”类型，不会影响任何形状或形式的运行时。

意思是，如果删除特殊的 LiquidHaskell 类型注释并使用标准 GHC 编译它，生成的代码是否总是相同的？换句话说：LiquidHaskell 扩展只是编译时的吗？

如果是，这似乎是两全其美，还是 LiquidHaskell 在类型系统中的表现力不如 Idris，因此在没有运行时术语的情况下进行管理？

问题：

假设我们有一个乘客，其起点和终点分别表示为：

问题：

如何将类约束应用于起点不应等于终点的乘客？

PS： 我在 Scala 社区问过类似的问题，但没有得到任何答案。考虑到scala 的精炼库是受Haskell 精炼的启发，也听说过液体 Haskell，我想知道如何使用 Haskell 解决它？

问题

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

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

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

例子

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

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

LiquidHaskel 输出 >>结果：安全

LiquidHaskel 输出 >>结果：不安全

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

对于文本类型，它出错了

例子

预期结果： 结果：安全

LiquidHaskell 输出：结果：不安全

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

Liquid Haskell 使用类似{-@ ... @-}合约块的注释。是否可以（使用命令行选项、配置文件）指定使用单行注释样式，例如-- ...合同？

为什么这会通过 Liquid Haskell 验证？

这是否意味着与LH的观点Nat相同？Int

我正在尝试解决 LiquidHaskell教程中的一些练习。所以，我写了这个：

但我收到一个错误（对不起，请，这种格式，它是原始的 LH 错误格式）：

什么是正确的“合同” mymap？如何修复此错误？应该如何阅读/处理消息Main.Cons##lqdc##$select v == ds_d35c x？

我正在阅读本教程，但我不确定我是否正确理解了文本（或者它是否完全正确）。有一个例子：

以下谓词是有效的，因为它们编码了前件推理方式：如果您知道 a 蕴含 b 并且您知道 a 为真，那么 b 也一定为真：

和 ex6 很好，但 ex7 不是，它失败了a = falseand b = false。LH 将其报告为：

我也不明白他们对含义的定义：“你应该读 p ==> q 好像 p 是真的那么 q 也必须是真的”。它听起来不正确，因为它只断言一种情况：T -> T = T. 我在这里想念什么？可能是教程在“ex7”中有错误？