如何将参数限制为仅变体类型的一个变体

Question

假设我有两种类型，Vector2D 和 Vector3D 并且它们被标记（这是正确的术语，对吧？），我想编写一个仅在 [=12] 上运行的函数=]（或者 vector(two) 在这里更正确？），像这样：

type two;
type three;
type vector('a) = 
  | Vector2D(float, float): vector(two)
  | Vector3D(float, float, float): vector(three);

let first = (a: vector(two)) => {
  switch(a) {
    | (x, y) => x +. y
  }
}

let second = (Vector2D(x, y)) => {
  x +. y
}

let third = ((x, y): vector(two)) => {
  x +.y
}

first 和 second 函数禁止传递 Vector3D，就像我想要的那样，但它们会发出警告 "This pattern matching is not exhaustive"。

对于 first 我想知道为什么这不是详尽无遗的，我在这里没有将可能的选项限制为 Vector2D 吗？对于 second 我想原因与 first 相同，但是用这种语法怎么可能解决问题呢？

至于third，这个不编译因为"This pattern matches ('a, 'b) but vector(two) was expected"。为什么编译器期望这里有任何元组？是不是不能在函数参数中使用解构？

编辑：
结果证明有一个更简单的问题来证明我想要什么

type state = Solid | Liquid
let splash = (object) => {
  switch(object) {
    | Liquid => "splashing sounds. I guess."
    | Solid => "" // this should not even be possible in the context of this function, and I want to compiler to enforce this
}

Answer 1

您可以使用 polymorphic variants:

完成您想要的

type vector = [
  | `Vector2D(float, float)
  | `Vector3D(float, float, float)
];

let first = (a: [`Vector2D(float, float)]) => {
  switch(a) {
    | `Vector2D(x, y) => x +. y
  }
}

let second = (`Vector2D(x, y)) => {
  x +. y
}

如果您尝试将 `Vector3D 传递给任一函数，这将给您一个类型错误：

               ^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type [> `Vector3d(float, float, float) ]
       but an expression was expected of type [< `Vector2D(float, float) ]
       The second variant type does not allow tag(s) `Vector3d

首先请注意，示例中的 Vector2D 和 Vector3D 不是类型。它们是构造 vector('a) 类型值的构造函数。正如您正确指出的那样，它们有时也被称为 "tags"，并且该类型有时被称为 "tagged union" 而不是 "variant" 因为值包含一个标记，该标记指定使用哪个构造函数来构造它.标记是使用构造函数模式进行模式匹配时检查的内容。

您在示例中使用的不是普通变体，而是 Generalized Algebraic Data Type (GADT)（在 OCaml/Reason 中命名为 "Generalized Variant" 可能更恰当）， ~~它不起作用的原因是，虽然 GADT 允许您将特定类型分配给构造函数，但它不能以相反的方式工作。例如，您可以有多个指定 vector(two) 的构造函数。~~（编辑：这似乎是错误的，请参阅@octachron 的回答）

示例中的 first 或 third 函数均未编译，编译器需要一个元组，因为您使用的是元组模式而不是构造函数模式。 (x, y) 与 Vector2D(x, y) 不同。如果是，您将无法区分 Vector2D(float, float) 和 Line(point, point)，例如，后者包含完全不同类型的数据。

Answer 2

关于 GADT 部分，这里的问题是您使用的是 bucklescript 及其古老的 4.02.3 编译器版本。例如，以下代码在 OCaml ≥ 4.03 中工作得很好：

type two = Two ; 
type three = Three ;
/* Never define abstract types when you want to use them as type level tags,
  your code will only works inside the module defining them, and then
  fail due to injectivity problems.
*/

type vector('a) = 
  | Vector2D(float, float): vector(two)
  | Vector3D(float, float, float): vector(three);

let sum_2 = (Vector2D(x,y)) => x +. y
let sum_3 = (Vector3D(x,y,z)) => x +. y +. z 
let sum_any = (type a, x: vector(a) ) => switch (x) {
  | Vector2D(x,y) => x +. y;
  | Vector3D(x,y,z) => x +. y +. z
}

但它会在 4.02.3 上失败并出现详尽警告（这应该被视为错误），因为在 4.03 中才添加了带有反驳条款的 GADT 的详尽检查。

如何将参数限制为仅变体类型的一个变体

how to limit a parameter to only one variant of a variant type

pattern-matching

ocaml

algebraic-data-types

gadt

reason