标准 ML 多态排序

Question

我在 ML 方面非常缺乏经验，我无法理解这一点。

开始提问

多态排序

这个对列表执行插入排序的函数将比较函数less和要排序的元素列表l作为参数。代码编译运行正常：

fun sort(less, nil) = nil |
    sort(less, a : : l) =
       let

fun insert(a, nil) = a : : nil |
   insert(a, b : : l) = if less(a,b) then a : : (b: : l)
                                   else b : : insert(a, l)

in
    insert(a, sort(less, l))
end;

这个排序函数的类型是什么？简单解释一下，包括辅助功能插入的类型。您不必在此代码上运行 ML 算法；只需解释为什么普通的 ML 程序员会期望代码具有这种类型。 （问题结束）

我已经获得了排序函数的类型（通过在 SML 解释器中运行代码），但我无法获得关于插入的第二部分。

排序函数类型：

val sort = fn : ('a * 'a -> bool) * 'a list -> 'a list 

任何帮助将不胜感激。

Answer 1

你通过“作弊”弄清了sort的类型，让下一步更难了；不要走捷径。
（没有人通过偷看答案学到任何东西。）

但你可以通过以下方式找出insert：

你知道的

val sort = fn : ('a * 'a -> bool) * 'a list -> 'a list 

sort 的第二个参数是'a list。

在

insert(a, sort(less, l))

您可以立即看到它有一些类型 (X * Y) -> Z 用于 一些 X、Y 和 Z。

您将sort 的第二个参数-a 的第一个元素作为insert 的第一个参数传递。
由于sort 的第二个参数是'a list，因此该列表的第一个元素是'a。
所以X 是'a，我们现在知道insert 对于一些 Y 和Z 是('a * Y) -> Z。

insert 的第二个参数的类型——sort(less, l)——是众所周知的；这是'a list。
所以我们现在知道Y 是'a list，而insert 是('a * 'a list) -> Z 对于一些 Z。

剩下的就是返回类型，因为

insert(a, sort(less, l))

是sort 返回的内容，它必须与sort 具有相同的返回类型。
所以Z 是'a list。

综上，insert的类型是

('a * 'a list) -> 'a list