SML 类型推断的提示答案

【问题标题】：Hint for SML type inferenceSML 类型推断的提示
【发布时间】：2016-06-05 18:35:55
【问题描述】：

我是SML新手，我正在尝试在SML类型参考中练习。我正在尝试扣除以下类型：

a)fun add42 x =x+42
b)fun comp F G = let fun C x = G(F(x)) in C end
c)fun compA42 x = comp add42 x
d)val foo = compA42 add42
e)fun compCompA42 x = comp compA42 x

我认为前四个的解决方案是：

a)int->int
b)(a->b)->(b->c)->a->c
c)(int->a)->int->a
d)int->int

但我对最后一个有点困惑。有提示扣除最后一种吗？？

非常感谢。

【问题讨论】：

标签： sml type-inference

【解决方案1】：

让我们一步一步地手动完成：

fun compCompA42 x = comp compA42 x

这是一个函数，所以compCompA42 的类型为α -> β。
compCompA42的返回值必须与comp compA42 x的类型相同，即β = typeof(comp compA42 x)。
我们现在已经是comp最通用的类型了：

(a -> b) -> (b -> c) -> a -> c

现在，我们需要专门针对a -> b = typeof(compA42) 和(b -> c) = α 时的情况：

a -> b = typeof(compA42) = (int -> d) -> int -> d。从这个等式得出a = int -> d 和b = int -> d。
所以，α = b -> c = (int -> d) -> c 和 β = typeof(comp compA42 x) = a -> c = (int -> d) -> c。
最后，compCompA42 最通用的类型是

α -> β = ((int -> d) -> c) -> (int -> d) -> c.

请注意，您总是可以让一些 SML 解释器（例如 smlnj）向您显示类型：

- fun compCompA42 x = comp compA42 x;
val compCompA42 = fn : ((int -> 'a) -> 'b) -> (int -> 'a) -> 'b

它与我们手动获得的类型相同（只需将 d 重命名为 'a 并将 c 重命名为 'b）。

【讨论】：