打字很难

类型检查是在某种编程语言中使用给定程序并计算出所有变量和表达式是否都具有正确类型的过程，即将字符串分配给字符串，算术表达式只涉及数字等。一些语言还提供类型推理，任务是编译器自己找出正确的类型。根据语言的特点，类型检查和类型推断问题的范围从微不足道到无法确定。

一个决策问题是可判定的，如果对于任何输入，我们可以计算该输入是否在有限时间内满足该问题。可判定问题的例子包括素性测试和布尔可满足性。例如，暂停问题是不可判定的：我们不能检查程序是否在有限时间内无限长地运行。我们对编程语言的类型检查和类型推理问题很感兴趣：给定一些输入程序，它会进行类型检查吗？在给定一些程序的情况下，我们应该为表达式分配哪些类型，以便它可以进行类型检查？

Hindley-Milner(HM)类型系统是具有参数多态性的简单类型λ演算的类型系统，是许多函数式语言的基础。HM的类型检查是可判定和有效的，其复杂度与程序大小呈线性关系。类型推断比类型检查更困难，因为编译器必须解决程序中表达式产生的类型约束。这对于HM类型的系统是可判定的，但是问题本身是PSPACE-HARD和EXPTIME-COMPLETE，这意味着在最坏的情况下，它至少需要相对于输入大小的多项式量的额外空间和指数时间。幸运的是，当多态变量的嵌套深度有界时，类型推断算法是线性的，这是大多数应用程序的情况。有许多类型推理算法，其中最著名的是所谓的算法W。Hindley-Milner类型系统是因为许多函数式程序设计语言都是基于它的(变体)。

下面我已经编译了一个语言列表，以及这些语言中的类型检查/类型推断有多难。如果您发现错误或缺少一种语言，请提交有关您的语言、其类型检查复杂性以及支持您的声明的最佳资源的问题。我并不认为这里显示的属性是完整的，也不是正确的，它主要是我一直在收集的博客帖子的合并。

不可靠，无法决定，埃里克·利伯特(Eric Lippert)在这个问题上给出了一个很好的答案。其他有趣的事情包括使用C#类型检查器的SAT解算器。

可判定的，使用Hindley-Milner，但由于有趣的编译器错误：(String.length"；"；)^(-1)：int。

具有足够的1扩展：不可判定，因为系统F中的类型检查是不可判定的。存在哈斯克尔类型的图灵机。一个更简单的变体是实现滑雪演算。

无法决定，因为Java泛型是图灵完成的。Java 8或更高版本不健全，如Amin和Tate(2015)所示

不可判定，类型推断和类型检查都是如此，因为它允许等级为3的类型。在特征中还实现了一个Small妈的解释器。

无法决定，因为它承认一个类型级别的滑雪演算，不健全，如Amin和Tate(2015)所示。Scala2.13.3(撰写本文时的最新版本)也出现了同样的问题。

无法决定。TypeScript的类型系统被证明是图灵完整的，直到他们不允许使用自引用类型。然而，Robbie Ostrow写了一个检验Collatz猜想的程序，而且由于Collatz猜想的推广形式是不可判定的3，打字稿类型系统也是不可判定的。

不可决定，因为可以在编译时计算递归函数，因此需要编译器解决暂停问题。

类型检查和类型推断主要用于静态类型语言。虽然存在一些动态语言的扩展，为它们注入了静态类型检查，但这些扩展不是语言的一部分，其复杂性不取决于语言，而取决于扩展。

某些语言提供显式的未检查强制转换，类型检查器接受这些类型转换，并可能在运行时失败。例如，在C#和Java中从对象强制转换到某个子类，在Go中强制转换类型interface{}的值，或者在Haskell中使用unsafeCoells。我选择不考虑这种强制转换/强制转换，因为未经检查的向下转换是一种本质上不安全的操作，类型检查器保证不会涵盖它。

干得好！请在官方问题跟踪器上报告，详细说明哪里出了问题，我会尽快修复它。

仅使用RankNTypes就足以进行树桩推断。足够有趣的是，只有当N>；=3时，这才是不可决定的。↩