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

【问题标题】：Why is the type inferred for my ML function different than I expect?为什么为我的 ML 函数推断的类型与我预期的不同？
【发布时间】：2016-09-04 05:09:34
【问题描述】：

我创建的函数名为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

为什么会这样？

【问题讨论】：

标签： types type-inference ml

【解决方案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

【讨论】：