泛型的 F# 类型推断方法是什么？

Question

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

这样编译，id 是 '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

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

Answer 1

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

例如，如果您有：

let callWithTen f = f 10   

然后，最初，编译器分配类型使得callWithTen 具有'a 类型，f 具有'b 类型。它还收集了以下约束：

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

解决这些约束后，编译器会推断出callWithTen 的类型为(int -> 'b1) -> 'b1。

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

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

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

Answer 2

首先请注意，如果我们将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 可以是任何类型（甚至不必是相同类型），只要其中至少一个具有名为* 的静态成员与x 和y 相同类型的参数。 mul 的返回类型将与 * 成员的返回类型相同。

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

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