OCaml类型级Peano算术实现报类型构造器逃逸错误如何解决

问题根源 #

之前所有尝试的核心问题是返回类型注解不符合类型逻辑：你使用的'a nat/n3 nat是全称量化的类型变量，等同于声明该函数可以返回任意类型的自然数，这与Peano加法的性质矛盾——加法的返回值类型是唯一由两个入参的类型决定的，不是可由调用方任意指定的。

你需要先在类型层面定义加法的对应关系，描述两个输入类型与返回类型的映射规则，才能通过类型检查。

正确实现 #

完整的Nat模块加加法实现如下：

module Nat = struct
  type zero = Z
  type 'a succ = S
  type 'a nat =
    | Zero : zero nat
    | Succ : 'a nat -> 'a succ nat

  (* 类型级加法映射：('a, 'b) sum 代表 'a + 'b 的结果类型 *)
  type (_, _) sum =
    | Sum_zero : ('a, zero) sum constraint 'a = ('a, zero) sum
    | Sum_succ : ('a, 'b) sum -> ('a, 'b succ) sum constraint ('a, 'b succ) sum = ('a, 'b) sum succ
end

open Nat

(* 加法实现，类型注解明确返回值为两个入参的sum类型 *)
let rec add : type n1 n2. n1 nat -> n2 nat -> (n1, n2) sum nat =
  fun a b -> match b with
  | Zero -> a
  | Succ b' -> Succ (add a b')

这里定义的('a, 'b) sum类型是类型层面的加法函数，两个构造子刚好对应Peano加法的两条公理：

• Sum_zero对应公理：任意自然数加0等于它本身
• Sum_succ对应公理：任意自然数加succ(b)等于succ(该自然数加b)
  与函数实现的逻辑完全匹配，因此可以通过类型检查。

验证示例 #

你可以用以下代码验证加法的类型正确性：

(* 定义 1 和 2 的类型级自然数 *)
let one = Succ Zero
let two = Succ (Succ Zero)

(* 验证 1 + 1 = 2，类型检查会自动通过 *)
let () =
  let res = add one one in
  assert (res = two)

此时res的类型会被自动推导为(zero succ, zero succ) sum nat，也就是zero succ succ nat，和two的类型完全一致。

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