关于 haskell:Fundeps 和 GADT:什么时候可以确定类型检查?

关于 haskell:Fundeps 和 GADT:什么时候可以确定类型检查?

Fundeps and GADTs: When is type checking decidable?

我正在阅读一篇关于 Haskell 以及 HList 是如何实现的研究论文,并且想知道所描述的技术何时可以确定,何时不能确定类型检查器。另外,因为你可以用 GADT 做类似的事情,所以我想知道 GADT 类型检查是否总是可确定的。

如果你有引用的话,我更喜欢引用,这样我就可以阅读/理解解释。

谢谢!


我相信 GADT 类型检查始终是可判定的;它的推论是不可判定的,因为它需要更高阶的统一。但是 GADT 类型检查器是您在例如中看到的证明检查器的受限形式。 Coq,构造函数在其中建立证明项。例如,将 lambda 演算嵌入 GADT 的经典示例为每个归约规则都有一个构造函数,所以如果你想找到一个术语的范式,你必须告诉它哪些构造函数可以帮你找到它。停止问题已转移到用户手中 :-)


您可能已经看过这个,但在 Microsoft 研究中有一系列关于这个问题的论文:类型检查论文。第一个描述了 Glasgow Haskell 编译器中实际使用的可判定算法。


推荐阅读