代码之家 › 专栏 › 技术社区 › Jason Dagit

Fundeps和GADTs:什么时候可以判定类型检查?

gadt type-systems type-inference haskell

15

Jason Dagit · 技术社区 · 18 年前

我正在阅读一篇关于Haskell和HList是如何实现的研究论文,并想知道所描述的技术何时适用于类型检查器,何时不适用于类型检查器。另外,由于您可以对GADT执行类似的操作,我想知道GADT类型检查是否总是可判定的。

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

谢谢

2 回复 | 直到 15 年前

1

9

Jude Allred 18 年前

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

2

1

Nick Fortescue 18 年前

Type Checking papers . 第一个描述了格拉斯哥哈斯克尔编译器中实际使用的可判定算法。