如何使用类型约束实现基于元组编码的数值加法？

问题背景 #

我用元组类型编码自然数：

• 加1：用unit * 'a包裹（定义为plus1类型）
• 减1：提取元组的第二个元素（定义为minus1类型）
• 零：定义为unit * unit

具体类型定义如下：

type zero = unit * unit
type 'a minus1 = 'snd constraint 'a = unit * 'snd
type 'a plus1 = unit * 'a

目前这套编码可以正常工作，示例代码：

type one = zero plus1
type two = one plus1
type two' = zero plus1 plus1
type two'' = unit * (unit * (unit * unit))

let minus1 ((), n) = n
let plus1 n = ((), n)
let zero = ((), ())
let one : one = plus1 zero
let two : two = plus1 one
let two : two = plus1 (plus1 zero)
let two : two' = two
let two : two'' = two

我想通过左操作数减1、右操作数加1，直到左操作数为0的思路实现类型级加法。如果OCaml类型系统支持or约束，我想要的逻辑可以写成：

type ('a, 'b) plus = 'res
                (constraint 'a = zero constraint 'res = 'b)
            or  (
                 constraint  ('a_pred, 'b_succ) plus = 'res
                 constraint 'a_pred = 'a minus1
                 constraint 'b_succ = 'b plus1
            )

请问是否可以按照这个思路实现plus类型？

实现方案 #

OCaml的类型系统不直接支持这种or式的递归约束，但可以通过GADT（广义代数数据类型）结合递归类型约束来模拟你想要的分支逻辑，完全贴合“左减1、右加1直到左为0”的思路。

完整可运行代码 #

type zero = unit * unit
type 'a plus1 = unit * 'a
type 'a minus1 = 'snd constraint 'a = unit * 'snd

(* 用GADT编码加法的两种分支情况 *)
type ('a, 'b, 'res) plus_rule =
  | Base : (zero, 'b, 'b) plus_rule  (* 基础情况：0 + b = b *)
  | Rec : ('a minus1, 'b plus1, 'res) plus_rule -> ('a, 'b, 'res) plus_rule  (* 递归情况：a + b = (a-1)+(b+1) *)

(* 定义加法类型别名，关联GADT约束 *)
type ('a, 'b) plus = 'res constraint ('a, 'b, 'res) plus_rule = 'res

(* 测试验证 *)
type one = zero plus1
type two = one plus1
type three = two plus1

(* 验证 1 + 2 = 3：类型检查通过，说明加法逻辑生效 *)
let test_1_plus_2 : (one, two) plus = plus1 (plus1 (plus1 zero))
(* 验证 2 + 1 = 3：同样符合预期 *)
let test_2_plus_1 : (two, one) plus = plus1 (plus1 (plus1 zero))

核心原理 #

1. 基础分支：通过Base构造器定义当左操作数为zero时，加法结果等于右操作数，对应你思路中的第一个约束分支。
2. 递归分支：通过Rec构造器定义当左操作数非零时，将左操作数减1、右操作数加1，然后递归推导加法结果，对应你思路中的第二个约束分支。
3. 类型约束关联：通过type ('a, 'b) plus = 'res constraint ('a, 'b, 'res) plus_rule = 'res将加法类型与GADT的规则绑定，让OCaml类型检查器可以根据输入类型自动匹配分支并推导结果类型。

这种方式完全遵循你最初的思路，绕过了OCaml不支持or约束的限制，实现了类型级的自然数加法。

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