登陆

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

admin 2022-11-25 5人围观 ,发现0个评论

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

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

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

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

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

如果是的话,这似乎是两个世界中最好的,或者LiquidHaskell在类型系统中不像Idris那样具有表现力,因此没有运行时条款管理?

请发表您的评论
请关注微信公众号
微信二维码
不容错过
Powered By Z-BlogPHP