GADT模式匹配

Question

我最近一直在使用GADT，我想知道是否有人可以为我指出正确的方向，学习如何键入它，以便它可以编译，如果它可能的话，或者如果我过于复杂的事情。

我在这里看到了一些关于GADT模式匹配的其他答案，但这似乎有点不同。

我见过这样的事情来表示一个没有可能的值的类型：

module Nothing = {
  type t =
    | Nothing(t);
};

所以我想用它来锁定这个Exit.t类型，这样我就可以有一个Exit.t('a，Nothing.t)类型来表示成功案例，捕捉到没有可恢复的失败值这一事实。

module Exit = {
  type t('a, 'e) =
    | Success('a): t('a, Nothing.t)
    | Failure('e): t(Nothing.t, 'e);

这看起来还不错，直到我尝试为它编写一个flatMap函数。

  let flatMap: ('a => t('a1, 'e), t('a, 'e)) => t('a1, 'e) = (f, exit) =>
    switch (exit) {
    | Success(a) => f(a)
    | Failure(_) as e => e
    };
};

现在，推断类型Exit.t总是Exit.t(Nothing.t，Nothing.t)，我有点理解，因为失败案例中的类型将第一个类型设置为Nothing，而成功案例中的类型将设置第二个类型为Nothing。

我已经尝试了我所知道的一件事，使用type a使其中一些类型成为本地类型。我试着让type a a1 e和type a e离开'a1，但我似乎就是不能理解。

Answer 1

(我使用下面的OCaml语法，因为这个问题也被标记为"ocaml"，但同样的语法应该是合理的。)

首先，您的类型Nothing.t不是空的。循环值Nothing (Nothing (Nothing (...)))是一个有效的居民。如果您确实希望类型为空，请不要放置任何构造函数。

其次，正如您所猜到的，在flat_map中，Failure分支强制使用Nothing.t实例化'a1。这是没有办法的；这不是编译器的缺点，只是解释这段代码的唯一方法。

第三，你把事情搞得有点太复杂了，因为为了实现你的目标，Exit.t根本不需要是一个GADT。

下面是一个更简单的例子，它表明，如果Nothing.t实际上是空的，那么编译器正确地允许不相关的分支。

type nothing = |
type ('a, 'b) result =
  | Success of 'a
  | Failure of 'b
let only_success (x : ('a, nothing) result) : 'a =
  match x with
  | Success v -> v
  | Failure _ -> . (* this branch can be removed, as it is correctly inferred *)