7

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

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

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

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

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

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

4

1 回答 1

3

要回答您的问题：Liquid Haskell 允许您提供编译器之外的单独工具验证的注释。代码仍然以完全相同的方式编译。

但是，我对您提出的问题持怀疑态度。可以说，在某些情况下，该类型的某些残基必须在 Haskell 的运行时存活——尤其是在涉及多态递归时。考虑这个函数：

lots :: Show a => Int -> a -> String
lots 0 x = show x
lots n x = lots (n-1) (x,x)

无法静态确定使用show. 从类型派生的东西必须在运行时继续存在。在实践中，使用类型类字典很容易做到这一点。理论上重要的细节是在运行时仍然选择类型导向的行为。

于 2018-12-15T00:05:31.423 回答