Fundeps 和 GADT：类型检查何时可判定？
我正在阅读一篇关于 Haskell 以及 HList 是如何实现的研究论文，并且想知道所描述的技术何时对于类型检查器是可判定的以及何时不可判定。 另外，因为您可以使用 GADT 执行类似的操作，所以我想知道 GADT 类型检查是否始终是可判定的。
如果你有引用的话，我更喜欢引用，这样我就可以阅读/理解解释。
谢谢！
I was reading a research paper about Haskell and how HList is implemented and wondering when the techniques described are and are not decidable for the type checker. Also, because you can do similar things with GADTs, I was wondering if GADT type checking is always decidable.
I would prefer citations if you have them so I can read/understand the explanations.
Thanks!
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
我相信 GADT 类型检查总是可判定的； 这是不可判定的推理，因为它需要更高阶的统一。 但是 GADT 类型检查器是您在例如中看到的证明检查器的受限形式。 Coq，构造函数构建证明项。 例如，将 lambda 演算嵌入到 GADT 中的经典示例对于每个归约规则都有一个构造函数，因此，如果您想找到某个项的范式，您必须告诉它哪个构造函数会得到您的结果到它。 停止问题已转移到用户手中:-)
I believe GADT type checking is always decidable; it's inference which is undecidable, as it requires higher order unification. But a GADT type checker is a restricted form of the proof checkers you see in eg. Coq, where the constructors build up the proof term. For example, the classic example of embedding lambda calculus into GADTs has a constructor for each reduction rule, so if you want to find the normal form of a term, you have to tell it which constructors will get you to it. The halting problem has been moved into the user's hands :-)
您可能已经看到过这一点，但 Microsoft 研究中心有一系列关于此问题的论文： 类型检查论文。 第一个描述了 Glasgow Haskell 编译器中实际使用的可判定算法。
You've probably already seen this but there are a collection of papers on this issue at Microsoft research: Type Checking papers. The first one describes the decidable algorithm actually used in the Glasgow Haskell compiler.