类型推断的限制是什么？哪些类型的系统没有通用推理算法？
user141335
问问题
1469 次
2 回答
12
Joe Wells表明，对于 System F，类型推断是不可判定的，这是 Girard 和 Reynolds 独立发现的最基本的多态 lambda 演算。这是显示类型推断局限性的最重要结果。
这是一个尚未解决的重要问题：将广义代数数据类型集成到 Hindley-Milner 类型推断中的最佳方法是什么？每年西蒙·佩顿·琼斯（Simon Peyton Jones）都会提出一个新的答案，据说比前一年的答案要好。我还没有阅读 2009 年 3 月的版本，所以不能说我是否相信它会是确定的。
于 2009-08-09T16:01:46.963 回答
6
值依赖类型系统（或简而言之，依赖类型系统）可以描述如下类型：“在评估时（运行时），此变量的值将始终等于该变量的值，即用不同的评估过程计算”。从代码中自动推断出这种类型需要自动证明定理。如果您可以表达的定理集仅限于那些可自动证明的定理，那将不是问题，但在依赖类型语言的情况下，通常情况并非如此。
因此，依赖类型系统不能具有一般（和完整）类型推断。
我相信有人可以提供一个道德正式和完整的答案......
于 2009-08-09T13:01:34.683 回答