为什么为我的 ML 函数推断的类型与我预期的不同?

问题描述

我创建了一个名为 maptree 的函数.下面是我的代码:

I made function that's name is maptree. And below is my code:

datatype 'a tree = LEAF of 'a | NODE of 'a tree * 'a tree;
fun maptree(f, NODE(X, Y)) = NODE(maptree(f, X), maptree(f, Y))
| maptree(f, LEAF(X)) = LEAF(f X);

我希望 maptree 有类型

I expected maptree to have the type

 ('a -> 'a) -> 'a tree -> 'a tree

但是编译器推断的类型是

but the type inferred by the compiler is

 ('a -> 'b) * 'a tree -> 'b tree

为什么会这样?

推荐答案

Hindley-Milner 类型推断算法允许您获得比预期更通用的类型.

The Hindley-Milner type-inference algorithm allows you to get more general type than you expected.

当算法试图推断 maptree 的类型时，它假设 f: 'a ->;'b (因为您使用 f 作为函数).没有什么可以进一步限制 f 的类型.

When the algorithm tries to infer the type for maptree, it assumes that f: 'a -> 'b (from the fact you're using f as a function). And nothing restricts the type of f further.

例如，如果您按如下方式定义了 maptree 函数(我在 LEAF 案例中使用了 f 两次):

If you, for example, defined the maptree function as follows (I used f twice in the LEAF case):

fun maptree(f, NODE(X, Y)) = NODE(maptree(f, X), maptree(f, Y))
  | maptree(f, LEAF(X)) = LEAF(f (f X))

然后类型推断机制必须将 f 的类型限制为 'a ->'a(因为我们将函数的输出提供给它的输入).

Then the type-inference mechanism would have to restrict the type of f to 'a -> 'a (since we feed the output of the function to its input).

修改案例的SML/NJ输出:

The output of SML/NJ for the modified case:

val maptree = fn : ('a -> 'a) * 'a tree -> 'a tree

这篇关于为什么为我的 ML 函数推断的类型与我预期的不同?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！