LiquidHaskell与Idris中的运行时"类型术语"

Question

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

伊德里斯是一种依赖类型的语言,在很大程度上是很好的.但是我读到类型检查期间的某些类型术语可以从编译时"泄漏"到运行时,即使是强硬的Idris也会尽力消除这些术语(这甚至是一个特殊功能......).然而,这种消除并不完美,有时确实会发生.如果,为什么以及何时发生这种情况并未立即从代码中清除,有时会对运行时性能产生影响.

我见过人们更喜欢Haskells的类型系统,因为它不会发生在那里.完成类型检查后,即可完成.类型被"丢弃"并且在运行时不使用.

LiquidHaskell的故事是什么？与传统的Haskell相比,它增强了类型系统的功能.LiquidHaskell是否也为某些类型的"星座"注入运行时位,或者(我怀疑)只是在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。从类型派生的东西必须存活到运行时。实际上，通过使用类型类字典很容易做到这一点。理论上重要的细节是，在运行时仍然会选择类型导向的行为。