类型推断的限制是什么？答案

【问题标题】：What are the limits of type inference?类型推断的限制是什么？
【发布时间】：2009-08-09 12:01:17
【问题描述】：

类型推断的限制是什么？哪些类型的系统没有通用推理算法？

【问题讨论】：

【解决方案1】：

Joe Wells 表明类型推断对于 System F 是不可判定的，这是 Girard 和 Reynolds 独立发现的最基本的多态 lambda 演算。这是显示类型推断局限性的最重要结果。

这是一个尚未解决的重要问题：将广义代数数据类型集成到 Hindley-Milner 类型推断中的最佳方法是什么？每年西蒙·佩顿·琼斯（Simon Peyton Jones）都会提出一个新的答案，据说比前一年的答案要好。我还没有阅读 2009 年 3 月的版本，所以不能说我是否相信它会是权威的。

【讨论】：

那么算法 W 涵盖了系统 F 的最大可能子集，这是可判定的？
@ott：我不是一个头脑清醒的类型理论家，但我敢打赌我的 |- 符号系统 F 有多个不可比较的可判定子集。更不用说扩展的可能性（GADT、等式约束、限定类型）。对于头脑敏锐的人群来说，这是充分的就业机会:-)
@Norman Ramsey：很有趣。我不知道类型理论家是不是头脑清醒，但我看到的论文似乎离现实真的很远，我不知道类型理论是否会成为主流并被广泛接受；您仍然需要学习 ML 才能了解基础知识。

【解决方案2】：

值依赖类型系统（或简而言之，依赖类型系统）可以描述如下类型：“在评估时（运行时），此变量的值将始终等于该变量的值，这是用不同的评估过程计算的”。从代码中自动推断出这种类型需要自动证明定理。如果您可以表达的定理集仅限于那些可自动证明的定理，那将不是问题，但在依赖类型语言的情况下，通常情况并非如此。

因此，依赖类型的系统不能进行一般（和完整）类型推断。

我相信有人可以提供道德正式和完整的答案......

【讨论】：