1

我试图理解关于类型推断的规则，因为我想将它融入我自己的语言中，并且本着这种精神，我一直在玩 F# 的类型推断，下面的内容让我觉得很奇怪。

这会编译，并且idis 'a -> 'a，这（如果我没记错的话）意味着每次调用都使用“新鲜”类型。

let id x = x

let id1 = id 1
let id2 = id "two"

但是在使用运算符时，似乎第一次调用决定了该函数的签名。

在这里，mul被报告为int -> int -> int

let mul x y = x * y

let mul1 = mul 1 2
let mul2 = mul 1.1 2.2 // fails here

如果我重新排序它们，那么mul是float -> float -> float：

let mul x y = x * y

let mul2 = mul 1.1 2.2
let mul1 = mul 1 2 // fails here

你能解释一下（最好是非学术性的）规则是什么，也许从类型检查实现的角度来看它是如何工作的？每次引用它们时，它是否会遍历函数来检查它们的类型？还是有其他方法？

4

2 回答 2

6

mul首先请注意，如果我们声明为内联函数，则不会发生这种情况：

let inline mul x y = x * y

let mul1 = mul 1 2  // works
let mul2 = mul 1.1 2.2 // also works

这里推断的类型mul如下：

x: ^a -> y: ^b ->  ^c
    when ( ^a or  ^b) : (static member ( * ) :  ^a *  ^b ->  ^c)

这种类型意味着参数x和y可以具有任何类型（甚至不必是相同类型），只要其中至少一个具有名为的静态成员，该成员接受与和*相同类型的参数。的返回类型将与成员的返回类型相同。xymul*

mul那么，当不是 inline时，为什么不得到相同的行为呢？因为成员约束（即表示类型必须具有特定成员的类型约束）只允许在内联函数上 - 这也是为什么类型变量^前面有 a 而不是通常的': 表示我们正在处理不同的，类型变量的限制较少。

那么为什么存在对非内联函数的这种限制呢？因为 .NET 支持什么。诸如“T 实现接口 I”之类的类型约束可在 .NET 字节码中表达，因此可用于所有函数。诸如“T 必须有一个名为 X 且类型为 U 的特定成员”之类的类型约束是不可表达的，因此在普通函数中是不允许的。由于内联函数在生成的 .NET 字节码中没有相应的方法，因此它们的类型不需要在 .NET 字节码中表达，因此限制不适用于它们。

于 2019-05-25T14:24:23.967 回答
4

F# 类型推断的这一方面在学术上并不是特别优雅，但在实践中效果很好。F# 类型推断的工作方式是编译器最初将所有内容视为类型变量（泛型类型）并收集对它们的约束。然后它会尝试解决这些限制。

例如，如果您有：

let callWithTen f = f 10

然后最初，编译器分配类型，例如callWithTenhas type'a和fhas type 'b。它还收集以下约束：

  • 'a = 'a0 -> 'a1因为callWithTen在语法上定义为一个函数
  • 'a0 = 'b因为变量f是函数的参数
  • 'b = 'b0 -> 'b1因为变量f被用作函数
  • 'b0 = int因为 的论点f是一个int。
  • 'b1 = 'a1因为调用f的结果是callWithTen.

解决这些约束，编译器然后推断出callWithTen具有 type (int -> 'b1) -> 'b1。

当您+在代码中时，您无法完全确定数字类型到底是什么。其他一些 ML 语言通过+处理整数和+.浮点数来解决这个问题，但这非常难看，因此 F# 采用了不同的方法，这有点特别。

据我所知，F# 有一个约束'a supports (+)。因此，在您的情况下发生的事情（在稍微简化的描述中）add是一个函数'a0 -> 'a0 -> 'a0where 'a0 supports (+).

在处理其余代码时，编译器还会收集约束'a0 = int（在第一次调用时）和'a0 = float（在第二次调用时）。它首先解决了第一个问题，这很好（因为intsupports +），但是它在第二个约束上失败了，因为int != float它在那里报告了一个错误。

于 2019-05-25T13:04:16.807 回答