8

在研究F# 和 OCaml 之间的类型推断差异时,我发现他们倾向于关注主格类型系统与结构 类型系统。然后我发现了函数式编程语言的独特特征,其中将类型和类型推断列为不同的特征。

由于特征文章说 OCaml 和 F# 都使用我认为是标准算法的Damas-Milner类型推断,即不允许变化的算法,这两个特征如何关联?是不是 Damas-Milner 是构建两个类型推理系统的基础,但它们每个都根据类型修改 Damas-Milner?

我还检查了 Damas、Milner 和 Hindley 的 F# 源代码,但没有找到。搜索推断一词出现了类型推断的代码。

如果是这样,是否有任何论文讨论特定语言的每种类型推理算法的细节,或者我是否必须查看OCamlF#的源代码。

编辑

这是一个突出显示与 OCaml 和 F# 之间的类型推断相关的差异的页面。

4

3 回答 3

6

关于你的 DM 问题,你是对的。对于 F# 和 OCaml,DM 算法只是一种模式。类型检查器已扩展为支持自定义功能。在 OCaml 中,这些特性包括具有行类型、多边形变体、一流模块的对象。在 F# - .NET 类型系统互操作(类、接口、结构、子类型、方法重载)中,度量单位。我认为 F# 类型推断也以从左到右的方式倾斜,以允许更有效的交互式检查,因此一些代码令人惊讶地需要注释。

就类型检查和推理而言,OCaml 比 F# 更具表现力和直观性。SML 比它们中的任何一个都更接近于普通的 HM,但 SML 还具有一些针对某些运算符多态性和记录支持的扩展。

于 2012-09-11T12:04:27.460 回答
4

我相信当他们谈论 OCaml 中的结构类型时,他们可能指的是对象系统(“OCaml”的“O”部分)。OCaml 的非对象部分是非常标准的 ML 类型系统;这是不寻常的对象系统。

OCaml 中的对象系统与 F# 中基于 .NET 类的对象系统非常不同。在 OCaml 中,您可以直接创建对象而无需使用类。类基本上是创建对象的便利功能。创建后的对象(使用文字直接创建或使用类创建)没有其类的概念。

看看当你编写一个接受一个对象并在其上调用特定方法的函数时会发生什么:

# let foo x = x#bar;;
val foo : < bar : 'a; .. > -> 'a = <fun>

参数类型被推断为包含名为 的方法的抽象类型bar。所以它可以接受任何具有这种方法和类型的对象。

这就是他们说对象系统是结构化类型的意思。一个对象唯一重要的是它的方法集,它决定了它可以在哪里使用。所以兼容性只是基于方法的“结构”。而不是关于“阶级”的任何想法。

于 2012-09-10T22:41:27.603 回答
2

由于特征文章说 OCaml 和 F# 都使用我认为是标准算法的 Damas-Milner 类型推断,即不允许变化的算法,这两个特征如何关联?

Damas-Milner 算法(也称为算法 W)可以扩展,实际上,它的所有实际相关实现都添加了许多扩展,包括 OCaml 和 F#。

是不是 Damas-Milner 是构建两个类型推理系统的基础,但它们每个都根据类型修改 Damas-Milner?

没错,是的。特别是,OCaml 对 Damas-Milner 核心有许多不同的实验扩展,包括多态变体、对象、一流模块。F# 更简单,但也有一些 OCaml 没有的扩展,尤其是重载(主要是运算符)。

我不相信有描述 OCaml 或 F# 的整个类型系统的摘要论文。确实,我不知道有哪篇论文描述了当今的 F# 类型系统。对于 OCaml,您有许多不同的论文,每篇论文都涵盖不同的方面。我将从Jacques Garrigue 自己的出版物开始,然后按照其中的参考资料进行操作。

于 2012-09-14T22:05:35.670 回答