SML中将数字转换为nat类型时出现递归类型错误求助

问题根源 #

你定义的'a nat是多态类型，但自然数的递归结构要求Succ构造器必须持有另一个nat类型的值，而非任意类型参数'a。这种错误的类型定义导致编译器无法推断出合法的递归类型，进而抛出循环类型错误。

修正后的完整代码 #

datatype nat =
    Zero
  | Succ of nat
  ;

fun to_nat(v) = if v = 0 then Zero else Succ(to_nat(v - 1));

fun plus(n1,n2) =
  case n1 of
    Zero => n2
  | Succ(v) => Succ(plus(v, n2))
    ;

fun multiply(n1,n2) =
  case n1 of
    Zero => Zero
  | Succ(v) => plus(multiply(v, n2), n2)
    ;

val five = to_nat(5);
val six = to_nat(6);
val eleven = plus(five, six);
val thirty = multiply(five, six);

关键改动说明 #

1. 修正类型定义：将datatype 'a nat改为datatype nat，明确Succ构造器的参数是nat类型，形成合法的递归结构。
2. 函数逻辑无需修改：原有的to_nat、plus、multiply函数逻辑本身是正确的，修正类型定义后即可正常工作。

报错原因解释 #

原代码中，编译器尝试推断to_nat的返回类型时，发现Succ(to_nat(v-1))要求类型参数'a等于'a nat，形成了'Z = 'Z nat的循环依赖，因此抛出"circularity"（循环类型）错误。去掉多态类型参数后，递归结构清晰，编译器能正确推断出所有函数的类型。

内容的提问来源于stack exchange，提问作者Node.JS