问题标签 [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.
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。
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 版
ubuntu - 需要帮助在 Ubuntu 上安装 LiquidHaskell
对于我的学士论文，我想写一些关于 LiquidHaskell 的文章并做一些实验。我已经安装了 Haskell/GHC 和 CVC4 作为 SMT Solver。现在我正在尝试在我的 Ubuntu-Laptop 上安装液体包，但遇到了问题：
如果我尝试该命令cabal install liquid-platform，我会得到以下输出：
如果我走 git 路线
我收到此错误：
我将非常感谢您可以提供给我的所有帮助。
提前致谢， Noodlez
haskell - 什么语言有等式重写？
函数式程序效率低下的一个典型案例是reverse从规范编写的函数
使用关联性，可以得出一个有效的反向
但是，问题首先来自哪里？
- 我们指示特定的订单
++ - 由我们的语言定义的组合定义了我们的组合的顺序
++ - 我们的语言不知道法律，源于代码本身，也不知道效率的概念。
我们真正想做的是：
- 指定一个（函数）关系
++，由它的所有定律正确商化 - 为它使用关系组合，它隐藏了将使用哪个特定的括号
- 在使用站点，选择一个最适合我们的访问模式和目标的括号（在 的情况下
reverse，这意味着移动所有括号以匹配结果列表的构造方式）
是否有任何语言可以产生一些规律，并根据一些指标寻找最好的重写？