编码为模块递归的多态递归的类型推断答案

【问题标题】：Type inference for polymorphic recursion encoded as module recursion编码为模块递归的多态递归的类型推断
【发布时间】：2016-10-27 20:14:17
【问题描述】：

标准 ML 没有多态递归。在模块语言中添加递归允许我们使用内函子的固定点来恢复多态递归作为一种特殊情况。例如：

signature SEQ =
sig
  type 'a seq

  (* operations on sequences *)
end

functor BootstrapSeq (S : SEQ) =
struct
  datatype 'a seq
    = Nil
    | Zero of ('a * 'a) S.seq
    | One of 'a * ('a * 'a) S.seq

  (* operations on sequences *)
end

structure rec Seq = BootstrapSeq (Seq)

众所周知，多态递归使类型推断无法确定。但是，函子定义已经包含部分类型信息，即其参数的签名。这些信息是否足以使类型推断再次可判定？

【问题讨论】：

什么实现支持structure rec？
@IonuțG.Stan：AFAICT，没有，虽然我没有尝试过 SML/NJ。
啊，所以这更像是一个理论问题。 SML/NJ 不支持。
@IonuțG.Stan，莫斯科 ML 支持它，但有一些限制。还有 OCaml，如果你愿意计算的话。

标签： recursion polymorphism sml type-inference ml

【解决方案1】：

是的，因为签名提供了多态类型的“前向声明”，所以不必递归推断。此外，您不需要仿函数，您可以直接编写递归结构绑定。但这需要一个签名注释，因此是相同的。

【讨论】：