问题标签 [liquid-haskell]

我正在读这个，我发现这个：

措施——为了让 Haskell 函数出现在细化类型中，我们需要将它们提升到细化类型级别。

还有其他文件声称需要采​​取措施才能在合同中使用此类功能。但我试过这个：

这有效，但len不是衡量标准。那么究竟什么是测量值，什么时候需要呢？

另一个不工作的例子measure：

我在许多文档中发现的 like 的使用{-@ measure length @-}会导致错误Cannot extract measure from haskell function（即 from length）。

我有代码：

当我在它上面运行 LH ( stack exec liquid -- MyFile.hs) 我得到错误：

我不知道这是什么意思，似乎 LH 认为调用T.head是不安全的。但我检查了长度T.length t > 0！解决此问题的规范方法是什么，以便 LH 可以通过验证？更有趣的是无需重写代码，仅使用 LH。

我正在关注 Liquid Haskell 教程：

这个例子失败了：

出现以下错误：

问题是为什么？守卫 (i < length vec) 应该确保 (vec ! i) 是安全的。

我正在关注Liquid Haskell 的官方教程，并偶然发现了其中似乎是一个“错误”。

以下代码出现在教程中， Liquid Haskell 应该检查它是否安全。

但是，在检查文件时，我得到：

我怎样才能检查这个属性？

我最近开始玩 Liquid haskell，在我能找到的所有教程中，我找不到像下面这样的任何例子。

如果我尝试以下操作，我的模块不会按预期进行类型检查：

但是，由于某种原因，以下仍然没有类型检查：

我得到了错误

此外，如果我省略了这getPerson _ = undefined条线，我会得到

尽管很明显这个函数是完全的，因为 Liquidhaskell 指定了先决条件。

我在这里做错了什么？我本质上只是希望能够对Maybe a来自Just构造函数的类型的子类型进行推理，但是我在任何地方都找不到任何可以正确执行此操作的示例。

我正在尝试从书中学习 Liquid Haskell 。为了测试我的理解，我想编写一个函数log2，它接受 2^n 形式的输入并输出 n。

我有以下代码：

但是在执行此代码时会出现一些奇怪的错误，即“精化中的排序错误”。我无法理解并解决此错误。

任何帮助将非常感激。

编辑：来自 Liquid Haskell 书：

谓词要么是原子谓词，通过比较两个表达式获得，要么是谓词函数对参数列表的应用......

在 Liquid Haskell 逻辑语法中，允许的谓词之一是：e r ewherer是原子二元关系（而函数只是一种特殊的关系）。

此外，在本教程中，他们将Even子类型定义为： {-@ type Even = {v:Int | v mod 2 == 0 } @-}

基于此，我认为elem应该工作。

但现在正如@ThomasM.DuBuisson 指出的那样，我想改写自己的elem'，以避免混淆。

现在，据我了解，为了能够将其elem'用作谓词函数，我需要将其提升为度量。所以我添加了以下内容：

现在我在类型定义中替换elem为. 但我仍然得到与前一个相同的错误。elem'Powers

这是一个计算给定列表中数字平均值的简单函数。

不幸的是，这段代码没有进行类型检查。

但是，如果我nonEmpty在定义函数后声明为度量，则它可以工作：

那么有人可以解释为什么会这样吗？

继我最近的问题之后，我一直在思考以下问题：

我们可以在 LH 中创建一些新的惊人类型，特别是表达一些非平凡的整数子集。例如：

但是现在我可以在 LH 中表达哪些其他重要的子集？

我可以在 LH 中创建一个仅包含 2 次方的类型吗？这是我最后一个问题的内容，似乎答案是否定的。

所以一个自然的问题是我可以表达什么样的子集（整数）？有没有很好的性格特征？

我正在关注LH 教程，并且坚持练习以改进过滤器函数的类型，如果使用具有唯一元素的列表调用，则输出也是具有唯一元素的唯一列表。

这是我正在使用的代码：

但是，当让 LH 证明它时，LH 会抛出以下错误：

我已经尝试以不同的方式指定它，在细化中使用 if 并使用不同的细化类型，但似乎都不起作用......

你能指出我正确的方向吗？我仍然很难理解错误消息。据我了解，推断的类型包含它是唯一的信息，如果xs'是唯一的，所以在我看来，这应该是所需类型的子类型。

我正在编码（作为假设）函子恒等律，如下所示：

我看不出这个公式有什么问题，但是我从 LH 那里得到了这个错误：

我究竟做错了什么？我的目标是用可扩展性来表述这个无点，但至少这个逐点表述应该首先起作用。

配置：

• GHC 版本：8.10.1
• 阴谋集团版本：3.2.0.0
• Liquid Haskell 版本：0.8.10.2