具有约束的内联记录构造函数的存在类型

Posted 2021-04-11

我试图在OCaml中表示一组语法的产生，而存在类型对于模拟语法规则的语义动作非常有用。我一直在研究Menhir源代码，存在类型也用于模拟语义动作。考虑以下：

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参数的约束，其中'a的action统一到'a的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中做到这一点。

答案

我不确定你想要什么。假设有一个函数'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 -> unit类型的操作一样有用。

另一答案

生产规则的语义动作应该有一些效果，否则根本不需要动作。您可以使用某种状态monad或直接在OCaml中对此效果进行编码，即作为可变引用或直接I / O。

在你的情况下，存在主义

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

具有产生'b类型值的效果。这与存在主义的定义直接相矛盾，因为在这种情况下，b需要逃避背景。所以正确的定义是

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

或者，如果你愿意使用一些monad，那么你需要将monad构造函数放在prenex位置

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

或者在模块级别绑定它：

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

您可以使用新操作扩展存在性，前提是它们不会泄漏存在量化的类型变量。

事实上，你可能只使用一流的模块，因为他们have existential type。例如。，

module type Semantics = sig 
   type t 
   val action : t -> unit
   val rule : t expr
end

type production = (module Semantics)

作为最后一点，考虑Oleg Kiselyov'tagless embedding作为GADT代表的替代品。请记住，解析器只是一个解释器:)