什么是类型推断的限制？

Question

哪些类型推断的限制？哪种类型的系统没有一般推理算法？

Answer 1

乔韦尔斯表明类型推断是不可判定为系统F，这是最基本的多态演算，由吉拉德和雷诺分别独立发现。这是示出了类型推断的限制最重要的结果。

下面是这仍然是开放的一个重要的问题：什么是广义代数数据类型融入辛德米尔纳类型推断的最好方法？每年西蒙·佩顿 - 琼斯来了一个新的答案，按理说它是比上一年的回答更好。我没有看过2009年3月版，因此不能说，如果我相信这将是明确的。

Answer 2

一个值相关的类型的系统中（或者，在短，依赖型系统）可以描述类型的说这样的话：“在评价时间（运行时），该变量的值将总是等于该变量的值，其计算与不同的评价过程”。自动推断该类型从代码需要定理的自动证明。如果设定您可以表达仅限于那些自动证明的定理，这不会是一个问题，但在依赖类型语言的情况下，这是通常情况并非如此。

所以依赖性输入系统不能有一般（和完整）类型推理。

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