我正在阅读有关Haskell以及HList是如何实现的研究论文，并且想知道所描述的技术何时对于类型检查器是可决定的，而不是可确定的。另外，由于我们可以使用GADT执行类似的操作，因此我想知道GADT类型检查是否总是可以确定的。

如果我们有引文，我希望予以引用，这样我才能阅读/理解其中的解释。

谢谢！

解决方案

回答

我们可能已经看过了，但是Microsoft研究中有关于此问题的一系列论文：Type Checking论文。第一个描述了在格拉斯哥Haskell编译器中实际使用的可判定算法。

回答

我相信GADT类型检查总是可以决定的；这是无法确定的推断，因为它需要更高阶的统一。但是GADT类型检查器是我们在例如中看到的证明检查器的受限形式。 Coq，构造函数在其中构建证明项。例如，将lambda演算嵌入GADT的经典示例为每个归约规则都有一个构造函数，因此，如果要查找术语的正常形式，则必须告诉它哪些构造函数可以解决这个问题。停止问题已移至用户手中：-)