polymorphism - 带约束的内联记录构造函数的存在类型

Question

我试图在 OCaml 中表示一组语法的产生式，存在类型对于建模语法规则的语义 Action 非常有用。我一直在研究 Menhir 源代码，存在类型也用于建模语义 Action 。考虑以下因素:

type 'a 'b production = { name: string; rule: 'a expr; action: 'a -> 'b }

产生式具有名称、返回 'a 的规则以及接收 'a 并返回 'b 的操作。简单参数类型的问题在于，产生式列表根本不可能是多态的，因此我可以在同一个列表中拥有一个 string_of_float 操作和另一个 string_of_int 操作；这是一个常见问题，可以通过显式 Ɐ 解决，例如，操作可以是:

action: 'a 'b. 'a -> 'b

但我还需要基于expr的参数进行约束，其中action的'a统一为' a of expr，因此，只要我们可以在代数数据类型中拥有内联记录构造函数，我们也应该能够在广义代数数据类型中拥有它们，对吗？

type production = (* Ɐ a. b. *)
  | Production: { name: string; rule: 'a expr; action: 'a -> 'b } -> production

但这不是有效的表单。我现在找到的解决方案是使规则也具有操作类型，例如:

type 'a expr =
  | Terminal of string * ('a -> 'a)
  | Sequence of 'a expr list * ('a list -> 'a)

但是这种单态性仍然具有很大的限制性。如何在具有共享约束的记录内对存在类型进行建模，以便我可以在不同的产品中拥有不同的返回类型，其中仍然可以对应用程序进行编译时检查(通过详尽的模式匹配)？

使用相同的逻辑，如果我想获得 'a 'b 中的函数列表。 -> 'a -> 'b，我是否需要使用存在类型构造函数来执行此操作(例如 [string_of_int; string_of_float])？

我相信我需要某种类型的限制(它们都是 * -> *)，但我来自 Haskell，但仍然不知道如何在 OCaml 中做到这一点。

Answer 1

我不确定你想要什么。假设有一个函数'a expr -> 'a，如果你想要一个具有不同内部表达式的产生式列表，你可以将产生式定义为

type 'r production = 
 | P: { name: string; rule: 'a expr; action: 'a -> 'r } -> 'r production

然后你就可以得到一个 [P string_of_float; 的列表； P string_of_int] 同时仍然知道操作的结果类型。 (此外，您之前的定义是有效的。)

其他通用量化让我觉得有问题:唯一具有 ∀'a∀'b 类型的函数。 'a -> 'b 是

的变体

let fail _ = assert false

同样，存在量化操作的返回类型意味着您永远无法恢复有关此返回类型是什么的信息，换句话说，它与仅具有类型的操作一样有用'a -> 单位。