如何修复OCaml代码中的Unbound constructor O错误？

你遇到的Unbound constructor O错误原因很直接——OCaml根本不知道O和S这两个构造器是什么！因为你还没有定义用来表示自然数的代数数据类型（ADT），这两个构造器属于该类型的一部分，必须先声明类型才能使用。

修正步骤 #

1. 先定义自然数类型
   首先要告诉OCaml，我们的nat类型由两个构造器组成：O表示零，S表示后继（接受一个nat类型的参数）。添加这行核心定义：

   type nat = O | S of nat
   

2. 修正原函数并补充类型标注（可选但更清晰）
   把你的三个函数放在类型定义之后，还可以加上类型标注让代码可读性更强：

   type nat = O | S of nat
   
   (* int -> nat：将整数转换为nat类型 *)
   let rec natadd_nat (c : int) : nat =
     match c with
     | 0 -> O
     | _ -> S (natadd_nat (c - 1))
   
   (* nat -> int：将nat类型转换为整数 *)
   let rec natadd_int (c : nat) : int =
     match c with
     | O -> 0
     | S n' -> 1 + natadd_int n'
   
   (* nat -> nat -> nat：实现两个nat类型的加法 *)
   let natadd (a : nat) (b : nat) : nat =
     natadd_nat ((natadd_int a) + (natadd_int b))
   

测试示例 #

现在运行你给出的测试代码，就能得到预期结果了：

# let two = S (S O) ;;
val two : nat = S (S O)
# let three = S (S (S O)) ;;
val three : nat = S (S (S O))
# natadd two three ;;
- : nat = S (S (S (S (S O))))

额外优化建议 #

你的“转int相加再转回去”思路简单直观，但如果想更贴合纯函数式风格，也可以直接基于nat类型的构造器递归实现加法（不需要转int），这样既避免了int类型的范围限制，效率也更高：

let rec natadd_direct a b =
  match a with
  | O -> b
  | S a' -> S (natadd_direct a' b)

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