我试图在函数内部创建一个本地求和类型，然后返回所述求和类型，而无需在 main 中声明它。这可能吗？我不相信它是直接的，但我一直在尝试使用 GADT 和多态变体来尝试找到解决方法，但我对 OCaml 仍然相当陌生，并没有完全理解它们。
我想要该函数执行以下操作。给定一个类型为 的元组，返回第一个元素，但其类型为和('a, 'b)之间的总和。'a'b
从加莱的回答来看，我尝试与 合作type ('a, 'b) either = | Left of 'a | Right of 'b，但未能使其发挥作用。
编辑：为了回应 glennsl 的评论，我试图解决的问题是针对我的课程项目的。我正在尝试实现构造逻辑和程序之间的柯里-霍华德同构。我目前已经使定理证明器和程序提取正常工作，但在处理析取规则时，我正在努力将程序的抽象形式转换为 OCaml 代码。我使用的规则集来自本文档的第 34 页。我已经添加了析取规则的图片。
我问的例子是定理 (anb) -> (avb)。有两个有意义的证明，我选择了使用 vIL 规则的一个，它对应于将 A 类型的变量左和注入到具有两个组件 A 和 B 的 sum 类型中。定理（使用此规则）是一个函数，它接受一个元组并返回第一个元素，但总和类型为 A + B。我希望获得此示例函数的 OCaml 代码的帮助。一旦我理解了这一点，希望我能够概括它。