问题标签 [liquid-haskell]

是否有带注释的变体或 Haskell Prelude 可用于轻松迁移调用head或之类的函数的现有程序length？

我正在尝试在关于懒惰队列的 LiquidHaskell 案例研究中做第一个练习

okHd失败：

从错误消息中，我很确定我没有向 LH 提供足够的信息以使其“知道”okList非空，但我不知道如何解决它。

我尝试用后置条件（？）明确地告诉它：

但这不起作用：

我在用 LiquidHaskell 证明以下定律时遇到了麻烦：

它被称为（之一）德摩根定律，并且简单地指出or两个值的否定必须与每个值and的否定相同。它已经被证明了很长时间，并且是 LiquidHaskell教程中的一个示例。我按照教程进行操作，但未能通过以下代码：

运行时liquid Test.hs，我得到以下输出：

现在我绝不是 LiquidHaskell 专家，但我很确定一定有问题。几年前我已经说服自己该身份成立，但为了确保我用所有可能的输入调用了该函数，并最终运行

所以我在 Haskell 代码中似乎没有错字，错误一定在 LiquidHaskell 规范中。似乎 LiquidHaskell 无法推断出结果Bool是严格的TRUE：

我的错误是什么？任何帮助表示赞赏！

PS：我正在使用z3求解器，并运行 GHC 7.10.3。LiquidHaskell 版本是2009-15.

我正在使用 Liquid-haskell 做一些实验，看看我可以用它做什么样的整洁的事情，但我遇到了一些困难。基本思想是我有一些功能需要在经过一定时间后过期的访问令牌。我正在尝试了解如何使用liquid-haskell 来确保在将令牌传递给我的一个函数之前检查其有效性。我在下面创建了一个最小的工作版本来演示我的问题。当我在这个文件上运行液体时，我收到以下错误：

我似乎无法弄清楚为什么会出现这个错误并且我尝试过的一切都失败了。有人可以帮我吗？

另外，我想将时间包中的 currTime 函数替换为 getCurrentTime 函数。这样我就可以将令牌上的时间戳与当前时间进行比较。这意味着我的 isExpired 函数将是 Token -> IO Bool 类型。这甚至可以使用液体哈斯克尔吗？

谢谢！

我有一个使用堆栈构建的项目并且需要 GHC 8。鉴于它需要 GHC 8，是否可以在我的项目中使用 Liquid Haskell？如果是这样，我应该如何安装和执行 Liquid Haskell？

谢谢！

我正在尝试为Data.Ratio模块编写一些规范。到目前为止，我有：

我正在验证的代码是：

代码被认为是安全的，因为 denominator 从不返回负值。

我觉得这很奇怪，因为我可以只写x <= 0一个后置条件，根据Data.Ratio模块的文档，这是不可能的。显然 Liquid Haskell 没有将我的后置条件与denominator.

我的理解是，由于没有检查函数实现，我最好使用假设关键字：

但是，我得到：

我的问题是

1. assume如果 LH显然没有通过与函数实现的比较来验证我的精炼类型的正确性，那么 LH 不应该强迫我在这种情况下使用关键字吗？
2. 我认为我应该使用assume关键字是否正确？
3. 怎么a突然不是数字了？我不使用的时候不是数字assume吗？

我正在尝试在 NixOS 上使用 Liquidhaskell。我可以安装包（liquidhaskell-0.8.2.3），虽然不是 cabal 集成，因为它需要 cabal 1.18-1.25，但我有 cabal 2.0.1.0。

我已经安装了liquidhaskell 包作为 ghc-with-packages 设置的一部分：

其中，包文本也安装在这个集合中：

但是，液体看不到这一点：

以上不是阴谋集团的一部分（试图从等式中消除阴谋集团的东西）。

我已经尝试使用 nix-shell 来完成这项工作，但是 nix-shell 或液体会在语言编译指示上崩溃：

感激地收到任何帮助。

我在 Haskell 中有一个响应 Json 输入的服务器。问题是在某些情况下服务器会因为部分功能而崩溃，但 Liquid Haskell 表示它是安全的。

这是一个最小的工作示例：

Liquid Haskell 说这是安全的，但我可以通过访问http://localhost:3000/ {"dim1":2} 使其崩溃。

我希望 Liquid Haskell 告诉我“dim1”函数的注释无效，因为它不能确定输入是 0 还是 1。

编辑：

我发现如果我在 Input 中手动为 dim1 创建一个访问函数，例如：

并使用它而不是“dim1”函数，然后我从 Liquid Haskell 获得所需的警告，即代码不安全。

我正在努力在 Ubuntu 18.04 中安装液体 Haskell。我尝试了几个命令来安装依赖项，现在在液体 Haskell 的最终编译中出现错误。

我正在使用以下命令进行安装：

阴谋集团安装liquidhaskell

我得到的错误是：

我也尝试将 Liquidhaskell 版本降级为 7 和 6，但没有运气。有人可以帮我安装吗？

感谢您提前提供的帮助和时间。

谢谢。