## 类型检查与类型的局限性 - 摘要 一篇1989年的论文指出，确定一个‘类型’是否为有效类型是不可判定的——类似于停机问题。这是因为类型系统很容易陷入循环，其中一个类型是其自身更大版本的子类型，无限增长。 解决方案，如讨论所示，在于限制类型：只有“小”类型（不包含抽象类型）才被认为是真正的类型。这类似于数学中“集合”和“类”的区别。 讨论深入探讨了依赖类型（函数的类型取决于其输入值）以及“所有类型的类型”的概念。围绕这个想法存在混淆，Python的例子说明了一个类型*可以*是‘Type’类型的值。 诸如类型层次结构（使用Lean和Rocq中的宇宙）和受限的依赖类型系统（如Liquid Types）等解决方案试图解决这个不可判定性问题，但通常以牺牲表达力为代价，或者只是推迟了问题。最终，完全类型级别的泛型函数仍然是一个挑战。