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

Question

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

有这样的语言吗？如果是,它的类型系统有任何限制吗？

更新1:为了非常清楚,我问的是静态类型的,完全类型推断的编程语言,而不是动态类型编程语言.

Answer 1

什么是类型推断？

从历史上看,类型推断(或类型重构)意味着可以派生程序中的所有类型,而基本上不需要任何显式类型注释.然而,近年来,在编程语言主流中已经成为时尚,甚至将最简单的自下而上类型推导形式标记为"类型推断"(例如,autoC++ 11 的新声明).所以人们已经开始添加"完整"来引用"真实"的东西.

什么是完整类型推断？

语言可以在多大程度上推断类型,并且在实践中,几乎没有语言支持最严格意义上的"完整"类型推断(核心ML是唯一的例子).但主要的区别因素是,是否可以为没有附加"定义"的绑定派生类型 - 特别是函数的参数.如果你能写,比方说,

f(x) = x + 1

并且类型系统指出f例如具有Int→Int类型,那么调用这种类型的推理是有意义的.此外,我们谈论多态类型推断时,例如,

g(x) = x

自动分配通用类型∀(t)t→t.

类型推断是在简单类型的lambda演算的背景下发明的,并且多态类型推断(也就是20世纪70年代发明的Hindley/Milner类型推断)是声称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演算(也称为"System F")允许后者.但它是类型理论的标准结果,完整系统F的类型重建是不可判定的.欣德利/米尔纳击中了一个稍微不那么富有表现力的类型系统的甜蜜点,其类型重建仍然是可判定的.

还有更高级的类型系统功能,也使完整类型重建不可判定.并且还有其他一些可以使其保持可判定性,但仍然使其不可行,例如存在ad-hoc重载或子类型,因为这会导致组合爆炸.

Answer 2

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

在Haskell中,它的类型类与多态返回类型相结合:

readAndPrint str = print (read "asd")

这read是一个类型的函数Read a => String -> a,这意味着"对于a支持类型类Read的任何类型,函数read可以获取String并返回一个a.所以如果f是一个接受int的方法,我可以编写f (read "123")并将它转换为"123"到Int然后调用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.没问题.

如果您使用类型的方法定义类'a. 'a -> int,即可以采用任何类型的参数并返回int的方法,则会出现此问题.您不能将该类的对象作为参数传递,f因为它与推断的类型不匹配.如果要将f这样的对象作为其参数,唯一的方法是添加类型注释f.

所以那些是几乎完全类型推断的语言的例子,以及它们不是的情况.如果您从这些语言中删除有问题的功能,则可以完全输入类型.

因此,没有这种高级特征的ML的基本方言是完全类型推断的.例如,我假设Caml Light是完全类型推断的,因为它基本上没有类的OCaml(但是我实际上并不知道语言,所以这只是一个假设).