haskell - LiquidHaskell 与 Idris 中的运行时 "type terms"

Question

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

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

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

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

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

如果是的话，这似乎是两全其美，还是 LiquidHaskell 在类型系统中的表现力不如 Idris，因此无需运行时术语即可管理？

Answer 1

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

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

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

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