为什么类型推断对面向对象语言不切实际？

Question

我正在研究一种新的编程语言的想法,理想情况下我希望这种语言能够混合一些功能和程序(面向对象)的概念.

我对Haskell这样的语言非常着迷的事情之一是它是静态类型的,但你不需要注释类型(魔术感谢Hindley-Milner!).

对于我的语言我真的很喜欢这个,但是在阅读了这个主题后,似乎大多数人认为类型推断对于子类型/面向对象是不切实际/不可能的,但是我不明白为什么会这样.我不知道F#,但我知道它使用Hindley-Milner并且是面向对象的.

我真的想要对此进行解释,并且最好是关于面向对象语言无法进行类型推断的场景的示例.

Answer 1

添加到seppk的响应:对于结构对象类型,他描述的问题实际上消失了(f可以被赋予多态类型,如∀A≤{x:Int,y:Int} .A→Int,或者甚至只是{x:Int ,y:Int}→Int).但是,类型推断仍然存在问题.

根本原因在于:在没有子类型的语言中,类型规则对类型施加了相等的约束.在类型检查期间处理这些非常好,因为通常可以使用类型的统一来立即简化它们.然而,对于子类型,这些约束被推广到不等式约束.你不能再使用统一,至少有三个不愉快的后果:

因此,对于子类型的类型推断并非不可能(在90年代已有很多关于该主题的论文),但它不是很实用.

OCaml采用了一种更简单的替代方案,它使用所谓的行多态来代替子类型.这实际上是易处理的.

Answer 2

当使用标称类型(这是一个类型系统,其中两个成员具有相同名称且相同类型的类不可互换)时,会有许多可能的类型,如下所示:

let f(obj) =
    obj.x + obj.y

任何具有成员x和成员y(支持+运算符的类型)的类都有资格作为可能的类型,obj类型推断算法无法知道哪一个是您想要的类型.

在F#中,上面的代码需要一个类型注释.因此F#具有面向对象和类型推断,但不能同时进行(除了本地类型推理(let myVar = expressionWhoseTypeIKNow),它总是有效).