types - 什么是完全类型推断语言？和这种语言的局限性？

Question

据我所知，任何在编写函数或模块时不需要在源代码中编写类型注释的编程语言，如果该代码块是“类型正确的”，编译器将推断类型并编译代码。还有更多吗？

是否有这样的语言？如果是的话，它的类型系统有什么限制吗？

更新1:
只是为了真的很清楚，我问的是一种静态类型的、完全类型推断的编程语言，而不是动态类型的编程语言。

Answer 1

什么是类型推断？

从历史上看，类型推断(或类型重构)意味着程序中的所有类型都可以派生，而无需任何显式类型注释。然而，近年来，编程语言主流已经成为一种流行，甚至将最琐碎的自下而上类型推导标记为“类型推断”(例如，C++11 的新 auto 声明)。所以人们开始添加“完整”来指代“真实”的东西。

什么是完整类型推断？

语言可以推断类型的范围很广，实际上，几乎没有语言支持最严格意义上的“完整”类型推断(核心 ML 是唯一的例子)。但主要的区别因素是是否可以为没有附加“定义”的绑定(bind)派生类型 - 特别是函数的参数。如果你能写，说，

f(x) = x + 1

并且类型系统发现 f 例如具有 Int → Int 类型，则调用此类型推断是有意义的。此外，我们讨论多态类型推断，例如，

g(x) = x

自动分配泛型类型∀(t) t → t。

类型推断是在简单类型 lambda 演算的上下文中发明的，而多态类型推断(又名 Hindley/Milner 类型推断，发明于 1970 年代)是 ML 语言家族(标准 ML、OCaml 和可以说是 haskell )。

全类型推断的限制是什么？

Core ML 具有“完整”多态类型推断的优势。但它取决于其类型系统中多态性的某些限制。特别是，只有定义可以是通用的，而不是函数参数。那是，

id(x) = x;
id(5);
id(True)

工作正常，因为 id当定义已知时，可以给定多态类型。但

f(id) = (id(5); id(True))

不会在 ML 中键入 check，因为 id不能作为函数参数是多态的。换句话说，类型系统确实允许像 ∀(t) t → t 这样的多态类型，但不允许像 (∀(t) t → t) → Bool 这样的所谓高级多态类型，其中多态值用于一流的方式(为了清楚起见，甚至很少有明确类型的语言允许)。

显式类型的多态 lambda 演算(也称为“系统 F”)允许后者。但类型论的一个标准结果是，完整系统 F 的类型重构是不可判定的。 Hindley/Milner 找到了一个表达力稍差的类型系统的最佳点，对于该系统，类型重构仍然是可以确定的。

还有更高级的类型系统功能也使完整的类型重建无法确定。还有其他一些让它保持可判定但仍然使其不可行，例如临时重载或子类型的存在，因为这会导致组合爆炸。