Fundeps和GADT:什么时候类型检查可判定？

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

如果你有它们我更喜欢引用,所以我可以阅读/理解解释.

谢谢!

我相信GADT类型检查总是可判定的; 这是不可判断的推论,因为它需要更高阶的统一.但是,GADT类型检查器是您在例如中看到的证明检查器的限制形式.Coq,构造函数构建证明术语.例如,将lambda演算嵌入到GADT中的经典示例为每个缩减规则都有一个构造函数,因此如果要查找术语的正常形式,则必须告诉它哪些构造函数可以使用它.暂停问题已移至用户手中:-)