返回未命名的和类型

Question

我试图在函数内部创建一个本地求和类型，然后返回所述求和类型，而无需在 main 中声明它。这可能吗？我不相信它是直接的，但我一直在尝试使用 GADT 和多态变体来尝试找到解决方法，但我对 OCaml 仍然相当陌生，并没有完全理解它们。

我希望该函数执行以下操作。给定一个类型为

('a, 'b)

的元组，返回第一个元素，但其总和的类型介于

'a

和

'b

之间。

从 gallais 的回答，我尝试使用

type ('a, 'b) either = | Left  of 'a | Right of 'b

，但无法让它工作。

编辑：为了回应 glennsl 的评论，我试图解决的问题是针对我的课程项目的。我正在尝试在构造性逻辑和程序之间实现Curry-Howard同构。我目前已经使定理证明器和程序提取正常工作，但在处理析取规则时，我正在努力将程序的抽象形式转换为 OCaml 代码。我使用的规则集来自此document的第34页。我附上了一张的照片。

我问的例子是定理 (a n b) -> (a v b)。有两个有意义的证明，我选择了使用 vI_L 规则的一个，它对应于将 A 类型的变量左和注入到具有两个组件 A 和 B 的 sum 类型中。该程序表示根据这个定理（使用这个规则），是一个接受元组并返回第一个元素的函数，但其总和类型为 A + B。

为了完成，这里是该项目的 github。

Answer 1

说你想定义一个函数的本地类型并没有多大意义。函数体是一个表达式，即它是由值而不是类型组成的。您可以在模块中定义函数本地的类型。但模块中定义的构造函数不允许逃逸函数的作用域。

# let f x =
  let module M = struct type 'a t = T of 'a end in
   M.T x;;
Error: [...] The type constructor M.t would escape its scope

使用全局定义的类型，你的函数很容易编写：

type ('a, 'b) either = | Left  of 'a | Right of 'b

let f (a, b) = Left a

这是该函数的应用：

# f (3, "yes");;
- : (int, 'a) either = Left 3

我认为使用 GADT 或多态变体没有帮助。它们很复杂，但不允许违反范围规则，这是另一回事。

如果您需要的话，您可以使用 OCaml 模块系统来定义抽象类型。使类型和函数都成为模块的本地函数。