多态递归场景下局部抽象类型与显式多态的差异解析

核心差异：全称多态类型 vs 局部抽象类型 #

plop1的类型解析 #

plop1的类型标注是'a 'b 'c. 'a -> 'b * 'c，这是全称量化的多态类型，意思是：对于任意选择的类型'a、'b、'c，这个函数都能接收'a类型的参数，返回'b和'c组成的元组。

在函数体中：

• 调用plop1 ""时，编译器会为这次调用单独实例化多态类型：把'a替换成string，同时返回一个'b1 * 'c1类型的元组，取fst后得到'b1；
• 调用plop1 1时，又实例化另一个版本：把'a替换成int，返回'b2 * 'c2类型的元组，取snd后得到'c2；
• 最终plop1的返回值(fst ..., snd ...)类型是'b1 * 'c2，正好匹配标注里的'b * 'c（这里'b对应'b1，'c对应'c2）。

因为全称多态允许每次调用使用不同的类型实例，所以完全符合类型规则。

plop2的类型冲突 #

plop2用了(type a b c)声明局部抽象类型，这些类型a、b、c在整个plop2的函数定义范围内是固定的抽象类型，不是“任意可选”的。也就是说，plop2的逻辑是：给定一组固定的a、b、c，函数接收a类型参数，返回b*c类型结果。

但函数体里的调用出现了矛盾：

• 调用plop2 ""要求参数类型a必须等于string；
• 调用plop2 1又要求参数类型a必须等于int；
• 而局部抽象类型a是固定的，不可能同时既是string又是int，因此触发类型错误。

内容的提问来源于stack exchange，提问作者abitbol