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

Question

我创建了名为 maptree 的函数。下面是我的代码：

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 具有类型

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

但是编译器推断的类型是

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

为什么会这样？

Answer 1

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

当算法尝试推断 maptree 的类型时，它假定 f: 'a -> 'b（根据您将 f 用作函数的事实）。并且没有进一步限制 f 的类型。

例如，如果您按如下方式定义 maptree 函数（我在 LEAF 的情况下使用了两次 f）：

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

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

修改后的 SML/NJ 的输出：

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

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

Why is the type inferred for my ML function different than I expect?

types

type-inference

ml