关于ML类型推理的轶事(1994)

清单现在是最难的部分了：如何着手写呢？最明显的方法就是把清单的前半部分放在一处，后半部分放在-4-其他地方。这样做的问题是，如果不遍历列表，我们就不知道它有多大；因此有必要再次遍历它才能进行实际的拆分。避免这种两遍属性会很好。想了一会儿，我意识到这个问题就像把一副牌等分成两堆。如果我想通过切牌来做到这一点，我必须先数牌，但我可以交替发牌到牌堆上，直到我用完为止。这种洞察力使解决方案变得容易得多。拆分一个空列表会产生一对空列表。将只有一个元素的列表拆分可以得到一个只有一个元素的列表和一个空列表。使用Split递归地使用Split来生成包含多个元素的列表，这样可以将前两个元素拆分，并将它们放在结果列表的开头。再说一次，它#39；写起来比描述起来容易：Fun Split(Nil)=(nil，nil)|Split([x])=([x]，nil)|Split(x：：y：：ail)=let val(p，q)=Split(Tail)in(x：：p，y：：q)end另外，此函数按编写方式工作，稍加实验就能使我确信我是正确的。3_3.ML专家会注意到。Nil)=(p，q)|loop(p，q，[a])=(a：：p，q)|loop(p，q，a：：b：：rest)=loop(a：：p，b：：q，rest)in loop(nil，nil，x)end此函数速度更快，因为它是尾递归。它还具有在途中颠倒列表的副作用，从而产生不稳定的排序。通过在合并期间再次颠倒列表来恢复排序的稳定性是一项有趣的练习。这需要额外的技巧，即在奇数递归过程中，比较函数的意义必须颠倒过来，因为它随后被用来对a-5进行排序-将其全部放在一起安全地合并和拆分之后，编写排序本身似乎是一件简单的事情。(=。我们只遵循前面的描述：FUN Sort(Nil)=nil|Sort(X)=let val(p，q)=let val(p，q)in Merge(Sort(P)，Sort(Q))end，事实上，当我键入此程序时，编译器接受了它。然而，我注意到了一些非常奇怪的事情：我认为排序的类型是int list->；int list，因为前面对较少约束的定义只对整数列表起作用。令人惊讶的是，编译器报告的类型为'；a list->；int list换句话说，这个排序函数完全接受任何类型的列表，并返回一个整数列表，这是不可能的。输出必须是输入的排列；它怎么可能有不同的类型？读者肯定会发现我的第一个冲动很熟悉：我想知道我是不是在编译器中发现了一个错误！在进一步思考之后，我意识到这个函数还有另一种方法可以忽略它的参数：也许有时它根本就没有返回。事实上，当我尝试它的时候，确实发生了这样的情况：排序(Nil)没有变成nil，但是对任何非空列表进行排序都会进入无限的递归循环，一旦我看到这一点，就不难理解为什么了，例如，假设我们正在对一个只有一个元素的列表进行排序。我们将其拆分成一个单元素列表和一个空的list___反转列表。结果可以是一种快得多的排序，但肯定更难理解。-6-，然后尝试递归地对单元素列表进行排序。这种递归没有任何进展，因此计算永远不会结束。解决方法很简单：添加一个子句来排序以处理单元素参数。如果参数是多个元素，则Split肯定会减少它，因此这应该是有效的：Fun Sort(Nil)=nil|Sort([a])=[a]|Sort(X)=let val(p，q)=Split(X)in Merge(Sort(P)，Sort(Q))end编译器将此函数的类型报告为int list-&>int listas，并再次通过几个实验令人信服地表明它做了应该做的事情。现在很容易编写。我们只需减少参数来进行排序，并将Merge和Split函数设置为本地的：FUN SORT LESS NIL=nIL|SORT LESS[a]=[a]|SORT LESS x=let Fun Merge(nil，x)=x|merge(x as h：：t，y as h'；：t'；)=if less(h，h'；)THEN h：：Merge(t，y。，x)Fun Split(Nil)=(nil，nil)|Split([x])=([x]，nil)|Split(x：：y：：Tail)=let val(p，q)=Split(Tail)in(x：：p，y：：q)end val(p，q)=Split(X)in Merge(减少p排序，减少q排序)end此函数确实按预期工作，其类型为('；a*'；a-。列表->；a列表如果我们在测试之前编写了整个函数，并且犯了同样的错误，省略了行-7-|少排序[a]=[a]t