时间戳

首页 > 解决方案 > GADT 模式匹配

ocaml - GADT 模式匹配

问题描述

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

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

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

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

所以我想用它来锁定这个 Exit.t 类型，这样我就可以有一个 Exit.t('a, Nothing.t) 类型来表示 Success 情况，捕捉到没有可恢复的 Failure 值的事实。

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

标签： ocamlreason

解决方案

（我正在使用下面的 OCaml 语法，因为该问题也被标记为“ocaml”，但同样适用于 Reason。）

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

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

第三，你让事情变得有点太复杂了，因为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 *)

推荐阅读