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

【问题标题】：what is a fully type-inferred language? and limitations of such language?什么是完全类型推断语言？和这种语言的局限性？
【发布时间】：2012-08-16 22:46:32
【问题描述】：

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

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

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

【问题讨论】：

Python 和 Perl 浮现在脑海。它们不是编译语言，但这几乎不相关。在某些情况下，类型推断不能使用 DWIM——根据我的经验，Python 有点过于偏执，而 Perl 有点过于放松。
python 和 perl 是动态类型的编程语言，类型在 run-time 时绑定到值/vars，我问的是在编译时建立类型的语言 -时间静态类型，完全类型推断语言
您尝试阅读en.wikipedia.org/wiki/Type_inference 吗？还有全类型推断是什么意思？
@Euphoric 完全类型推断意味着没有类型无法在没有类型注释的情况下确定的表达式。
看看ACL2。它可能看起来像动态类型，但它允许推理代码的所有类型属性。当然，代价是不完全图灵完备。

标签： types programming-languages functional-programming type-inference type-systems

【解决方案1】：

什么是类型推断？

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

什么是完整类型推断？

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

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 中不进行类型检查，因为 id 不能作为函数参数多态。换句话说，类型系统确实允许像 ∀(t) t → t 这样的多态类型，但不允许像 (∀(t) t → t) → Bool 这样的所谓高级多态类型，其中多态值用于一流的方式（为了清楚起见，即使是极少数显式类型的语言也允许这样做）。

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

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

【讨论】：

【解决方案2】：

完整类型推断的局限性在于它不适用于许多高级类型系统功能。以 Haskell 和 OCaml 为例。这两种语言几乎都是完全类型推断的，但有一些可能会干扰类型推断的特性。

在 Haskell 中，它的类型类与多态返回类型相结合：

readAndPrint str = print (read "asd")

这里read是Read a => String -> a类型的函数，这意味着“对于任何支持类型类Read的类型a，函数read可以接受String并返回a .所以如果f是一个接受int的方法，我可以写f (read "123")，它将“123”转换为Int 123并用它调用f。它知道它应该将字符串转换为Int因为f 采用 Int。如果 f 采用 int 列表，它会尝试将字符串转换为 Int 列表。没问题。

但是对于上面的readAndPrint 函数，这种方法不起作用。这里的问题是print 可以接受可以打印的任何类型的参数（即支持Show 类型类的任何类型）。因此，编译器无法知道您是否要将字符串转换为 int、int 列表或任何其他可以打印的内容。因此，在这种情况下，您需要添加类型注释。

在 OCaml 中，有问题的特性是类中的多态函数：如果您定义一个函数，该函数将对象作为其参数并调用该对象的方法，编译器将为该方法推断出单态类型。例如：

let f obj = obj#meth 23 + obj#meth 42

这里编译器将推断obj 必须是一个类的实例，该类具有一个名为meth 类型为int -> int 的方法，即接受一个Int 并返回一个Int 的方法。您现在可以定义一堆具有此类方法的类，并将该类的实例作为参数传递给f。没问题。

如果您使用'a. 'a -> int 类型的方法定义一个类，即可以接受任何类型的参数并返回一个int 的方法，则会出现问题。您不能将该类的对象作为参数传递给f，因为它与推断的类型不匹配。如果你想让f把这样一个对象作为它的参数，唯一的办法就是给f加上一个类型注解。

所以这些是几乎完全类型推断的语言示例以及它们不是的情况。如果您从这些语言中删除有问题的功能，它们将被完全类型推断。

因此，没有此类高级功能的机器学习的基本方言是完全类型推断的。例如，我假设 Caml Light 是完全类型推断的，因为它基本上是没有类的 OCaml（但是我实际上并不了解该语言，所以这只是一个假设）。

【讨论】：

一个很好的答案，它实际上解释了为什么全类型推理很困难，因此并不完全可取。

【解决方案3】：

另一个限制是排名较高的类型。例如，以下程序不在具有 ML 风格类型推断的语言中进行类型检查：

foo = let bar f = (f ['a', 'b', 'c'], f [1,2,3]) in bar reverse

类型检查器可以为 f 分配类型 [Char] -> [Char] 或 [Int] -> [Int]，但不能分配给所有 a.[a]->[a]。在 ML、Ocaml 和 F# 中无法解决此问题，因为您甚至无法编写更高等级的类型。

但 Haskell（通过 GHC 扩展）和 Frege 支持更高级别的类型。但是因为只有更高等级的类型检查（与更高等级的类型推断相反）是可能的，所以程序员需要给出类型注释，例如：

foo = let bar (f :: forall a.[a]->[a]) = (f ['a', 'b', 'c'], f [1,2,3]) in bar reverse

【讨论】：