打字很难
类型检查是使用某种编程语言编写给定程序并确定所有变量和表达式是否具有正确类型的过程，即将字符串分配给字符串，算术表达式仅包含数字等。某些语言还提供类型推断，任务分配编译器的任务是自己找出正确的类型。根据语言的功能，类型检查和类型推断问题的范围从琐碎的到不确定的。
如果对于任何输入我们都可以计算输入是否可以在有限时间内满足问题，则决策问题是可以确定的。可判定问题的示例包括素数测试和布尔可满足性。例如，暂停问题无法确定：我们无法检查程序是否在有限时间内无限长地运行。我们对编程语言的类型检查和类型推断问题感兴趣：给定一些输入程序，它是否进行类型检查？并给出了一些程序，我们应该为表达式分配哪些类型以使其进行类型检查？
Hindley-Milner（HM）类型系统是具有参数多态性的简单类型lambda演算的类型系统，它被用作许多功能语言的基础。 HM的类型检查是可以确定和有效的，它的复杂度在程序大小上是线性的。类型推断比类型检查更困难，因为编译器必须解决程序中表达式产生的类型约束。对于HM类型的系统来说这是可以确定的，但是问题本身是PSPACE-hard和EXPTIME-complete，这意味着在最坏的情况下，它至少需要多项式数量的额外空间和相对于输入大小的指数时间。幸运的是，当多态变量的嵌套深度有界时，类型推论算法是线性的，就像大多数应用程序一样。存在许多类型推断算法，最著名的是所谓的算法W。许多功能性编程语言实现HM类型系统的变体。
用简单的术语来说，从属类型允许类型不仅取决于其他类型，而且还取决于值。通过一个示例可以最好地理解这一点：通常，我们只能编码非常粗糙的信息，例如“ x是整数类型”。依赖类型允许我们定义更详细的类型。例如，我们然后可以创建一个类型“偶数整数”，其唯一居民是偶数整数。严格来说，这比以前的设置要强大：从属类型通常使类型推断变得不确定，这可以通过简化“后对应问题”来说明。
下面，我列出了语言列表，以及这些语言的类型检查/类型推断的难易程度。如果您发现错误或缺少某种语言，请提出您的语言问题，其类型检查的复杂性，并且最好是一种可以支持您的主张的资源。我不主张此处显示的属性的完整性或正确性，这主要是我一直在收集的博客文章的合并。
听起来不妙，不确定，埃里克·利珀特（Eric Lippert）对这个话题有一个很好的SO答案。其他有趣的事情包括使用C＃类型检查器的SAT求解器
可以确定，使用Hindley-Milner，但由于一个有趣的编译器错误，目前还不完善：（String.length＆＃34;＆＃34;）^（-1）：Int
具有足够的1个扩展：不确定，因为系统F中的类型检查是不确定的。存在Haskell类型的图灵机。一个更简单的变体是实现SKI演算。
无法确定，因为Java泛型已完成。如Amin和Tate（2015）所示，Java 5或更高版本不健全。
不可确定的是，类型推断（因为Rust具有rank-3类型）和类型检查，如使用traits实现的Smallfuck解释器所示。
不确定，因为它承认类型级别的SKI演算是不健全的，如Amin和Tate（2015）所示。 Scala 2.13.3（撰写本文时为最新）也存在相同的问题。
不确定性：TypeScript的类型系统被证明是Turing完整的，直到他们禁止使用自引用类型。但是Robbie Ostrow编写了一个检查Collatz猜想的程序，并且由于Collatz猜想的广义形式是不可确定的3，因此TypeScript类型系统也是不可确定的。
不确定，因为可能在编译时评估递归函数，因此需要编译器解决停止问题。
类型检查和类型推断主要适用于静态类型的语言。尽管存在某些动态语言的扩展，使它们具有静态类型检查功能，但这些扩展不是语言的一部分，并且复杂度不取决于语言，而取决于扩展。
某些语言提供显式的未经检查的类型转换，这些类型转换会被类型检查器接受，并且可能在运行时失败。 例如，将对象从Object强制转换为C＃和Java中的某些子类，在Go中强制转换类型interface {}的值，或者在Haskell中使用unsafeCoerce。 我选择不考虑这种类型的强制转换/强制转换，因为未经检查的向下转换是一种天生的不安全操作，类型检查器保证不涵盖此操作。 做得好！ 请在官方问题跟踪工具上报告该问题，并详细说明问题所在，我将尝试尽快进行修复。 仅使用RankNTypes就足以推论。 有趣的是，这仅在N> = 3时才能确定。
