10

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

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

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

4

3 回答 3

15

什么是类型推断？

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

什么是完整类型推断？

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

f(x) = x + 1

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

g(x) = x

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

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

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

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 找到了一个表达力稍差的类型系统的最佳点，对于该系统，类型重构仍然是可以确定的。

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

于 2012-05-06T12:00:19.487 回答
13

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

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

readAndPrint str = print (read "asd")

这read是一个 type 的函数Read a => String -> a，这意味着“对于任何a支持类型类的类型，Read该函数read都可以采用 aString并返回 an 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必须是具有名为methtype的方法的类的实例int -> int，即采用 Int 并返回 Int 的方法。您现在可以定义一堆具有此类方法的类，并将该类的实例作为参数传递给f. 没问题。

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

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

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

于 2012-05-05T18:04:05.533 回答
2

另一个限制是排名较高的类型。例如，以下程序不会在具有 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
于 2012-05-07T09:00:55.483 回答