问题标签 [liquid-haskell]

问问题

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

34 问题
Newest
Active
Bountied
318
Unanswered
0 投票
0 回答
23 浏览

liquid-haskell - 列表数据类型的记录字段命名问题

为了演示，我有两个几乎相同的文件：ListSuccess.hs和ListFailure.hs：

这些文件之间的唯一区别在于ListSuccess将字段命名为Consaslh和lt，并将ListFailure字段命名为Consashead和tail。

用 编译liquid，ListSuccess.hs编译成功，但是ListFailure编译失败，产生这个错误：

据我所知，使用head和tail作为字段名称应该不是问题，特别是因为我导入了隐藏这些名称的前奏。即使我使用import qualified Prelude和类似的变体，也会发生同样的错误。

这是一个错误，还是我在这里遗漏了什么？

配置：

  • LiquidHaskell 版本 0.8.6.0。
0 投票
0 回答
21 浏览

liquid-haskell - 在等式推理中扩展函数的递归情况

上下文：我正在证明有关 Haskell 快速排序实现的一些属性。以下代码是定义非确定性permute函数所需的全部内容。请注意，我使用的是LList而不是 Haskell 的基本[]类型。问题领域是permute_LCons_expansion_correct定理（它不是一个定理）。

在permute_LCons_expansion_correct中，方程应该是正确的，因为中间的表达式只是LConscase的主体，permute也是 的定义permute_LCons_expansion。但是，当我编译时，我得到这个 LH 错误：

为什么 LH 不承认隐式相等？请注意，我使用的是(==.)fromLanguage.Haskell.Equational而不是Language.Haskell.ProofCombinators.

配置：

  • ghc 版本 8.10.3
  • LiquidHaskell 版本 0.8.6.0
  • 阴谋集团 3.2.0.0 版
0 投票
0 回答
65 浏览

ubuntu - 需要帮助在 Ubuntu 上安装 LiquidHaskell

对于我的学士论文，我想写一些关于 LiquidHaskell 的文章并做一些实验。我已经安装了 Haskell/GHC 和 CVC4 作为 SMT Solver。现在我正在尝试在我的 Ubuntu-Laptop 上安装液体包，但遇到了问题：

如果我尝试该命令cabal install liquid-platform，我会得到以下输出：

如果我走 git 路线

我收到此错误：

我将非常感谢您可以提供给我的所有帮助。

提前致谢， Noodlez

0 投票
0 回答
161 浏览

haskell - 什么语言有等式重写？

函数式程序效率低下的一个典型案例是reverse从规范编写的函数

使用关联性，可以得出一个有效的反向

但是，问题首先来自哪里？

  • 我们指示特定的订单++
  • 由我们的语言定义的组合定义了我们的组合的顺序++
  • 我们的语言不知道法律，源于代码本身，也不知道效率的概念。

我们真正想做的是：

  • 指定一个（函数）关系++，由它的所有定律正确商化
  • 为它使用关系组合，它隐藏了将使用哪个特定的括号
  • 在使用站点，选择一个最适合我们的访问模式和目标的括号（在 的情况下reverse，这意味着移动所有括号以匹配结果列表的构造方式）

是否有任何语言可以产生一些规律，并根据一些指标寻找最好的重写？


12345678910