OCaml函数内返回局部和类型实现问询（关联Curry-Howard同构）

核心问题拆解 #

你要实现的是函数内封装和类型（无需全局声明），接收('a, 'b)元组后返回第一个元素，且返回值类型为'a与'b的和类型——这完全匹配Curry-Howard同构中析取引入规则（∨I_L）的需求，对应定理(a ∧ b) → (a ∨ b)的程序实现。

可行方案 #

方案1：局部代数类型声明 #

直接在函数内部定义和类型，语法简单且类型约束明确：

let inject_left (a, _) =
  type ('a, 'b) either = Left of 'a | Right of 'b in
  Left a

该函数的类型为('a * 'b) -> ('a, 'b) either，完美满足需求：接收合取对应的元组，返回析取类型的左分支实例。

如果需要支持右注入（∨I_R规则），可以对称实现：

let inject_right (_, b) =
  type ('a, 'b) either = Left of 'a | Right of 'b in
  Right b

方案2：多态变体实现 #

无需显式声明局部类型，利用OCaml的多态变体自动推导和类型，代码更简洁：

let inject_left (a, _) = `Left a

函数类型为('a * 'b) -> [> Left of 'a ]，若需要严格约束为'a与'b`的和类型，可添加类型标注：

let inject_left (a, _) : [ `Left of 'a | `Right of 'b ] = `Left a

适配Curry-Howard场景说明 #

对于你提到的定理(a ∧ b) → (a ∨ b)，上述inject_left函数就是∨I_L规则对应的程序：元组对应逻辑合取（∧），和类型对应逻辑析取（∨），左注入操作正好对应从合取项推导至析取左分支的规则，可直接推广到你的定理证明器与程序提取流程中。

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