变体定义中的多态变体限制答案

【问题标题】：Polymorphic variant restriction in the variant definition变体定义中的多态变体限制
【发布时间】：2018-11-10 02:56:12
【问题描述】：

假设我想在 OCaml 中建模一个简单的表达式类型：

type expr = 
| `Int of int
| `Str of string
| `IntAdd of expr * expr
| `StrAdd of expr * expr

是否可以将expr * expr 中的expr 限制为expr 本身的特定构造函数（即我希望IntExpr 只允许'Int'）？我可以用模式模仿这个匹配，但在 expr 扩展后变得很麻烦。我能以某种方式使用OCaml的类型系统来实现这个？

我尝试使用多态类型上限如下：

type expr = 
| `Int of int
| `Str of string
| `IntAdd of [< `Int] * [< `Int]
| `StrAdd of [< `Str] * [< `Str]

但是编译器不接受这个（带有消息In case IntAdd of [< Int ] * ([< Int ] as 'a) the variable 'a is unbound）。有什么诀窍可以使这项工作发挥作用吗？

【问题讨论】：

这似乎是您在 Haskell 中使用 GADT 的那种事情：data Expr a where { Int :: Int -> Expr Int; Str :: String -> Expr String; IntAdd :: Expr Int -> Expr Int -> Expr Int; StrAdd :: Expr String -> Expr String -> Expr String }
mads-hartmann.com/ocaml/2015/01/05/…
最后一个链接真的很有帮助---谢谢！

标签： types ocaml polymorphic-variants

【解决方案1】：

给定的例子很简单，多态变体就足够了：

type int_expr = [`Int of int | `Add of int_expr * int_expr]
type string_expr = [`String of string | `Concat of string_expr * string_expr]
type expr = [int_expr | string_expr]

如果您想要更有趣的功能，例如多态数据结构，GADT 是必要的：

type _ expr =
  | Int : int -> int expr
  | Add : int expr * int expr -> int expr
  | String : string -> string expr
  | Concat : string expr * string expr -> string expr
  | Pair : 'a expr * 'b expr -> ('a * 'b) expr
  | Fst : ('a * 'b) expr -> 'a expr
  | Snd : ('a * 'b) expr -> 'b expr

错误消息的推理和可理解性受到 GADT 的影响，因此如果您决定使用它们，请准备好克服这些困难。

【讨论】：

谢谢--- GADT 似乎是一种正确的方法。
旁注：第一个具有多态变体的示例无法正常工作，因为`Add(`String("a"), `String("b")) 编译时没有任何问题。
@Ibrahim，当然，多态变体允许通过设计不受约束的构造。请注意，您描述的值将没有类型expr，并且在您尝试将其用作expr 时会出现类型错误，而不是在构造时。如果你想要更早的类型检查，你可以使用注解。