当 GADT 构造函数包含多个类型变量时，局部抽象类型的范围错误

Question

鉴于此 GADT

type _ t = 
  | A : (string -> 'ok) * (string -> 'err) -> ('ok, 'err) result t

为什么这会失败并出现“类型构造函数会超出其作用域”错误

let f (type a) (gadt: a t): a Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, _) -> Ok (ok response))

Error: This expression has type [=12=] but an expression was expected of type 'a
       The type constructor [=12=] would escape its scope

而这个只是将模式匹配提取到一个单独的函数中的方法有效吗？

let parse (type a) (gadt: a t) (response: string): a = 
  match gadt with
  | A (ok, _) -> Ok (ok response)
                     
let f (type a) (gadt: a t): a Future.t = 
  Future.bind (fetch ()) (parse gadt)

第一个示例也适用于更简单的 GADT，例如

type _ t =
  | B : (string -> 'a) -> 'a t

表明 GADT 构造函数与多个类型变量、局部抽象类型和闭包之间存在一些奇怪的交互。

这已经在从 4.06 到 4.14 的多个 OCaml 版本上进行了测试，结果相同，因此至少看起来不太可能是错误。

完整示例

module Future = struct
  type 'a t

  let bind : 'a t -> ('a -> 'b) -> 'b t = Obj.magic
end
  
let fetch : unit -> 'a Future.t = Obj.magic

type _ t = 
  | A : (string -> 'ok) * (string -> 'err) -> ('ok, 'err) result t

let parse (type a) (gadt: a t) (response: string): a = 
  match gadt with
  | A (ok, _) -> Ok (ok response)
                     
let f_works (type a) (gadt: a t): a Future.t = 
  Future.bind (fetch ()) (parse gadt)

let f_fails (type a) (gadt: a t): a Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, _) -> Ok (ok response))

编辑：扩展示例

上面的例子有点过于简单了，虽然它确实很好地说明了潜在的问题，但它并没有表明我确实需要抽象整个 ('ok, 'err) result 类型，因为那里是具有其他形状的其他构造函数，此处由附加 B 构造函数说明：

type _ t = 
  | A : (string -> 'ok) * (string -> 'err) -> ('ok, 'err) result t
  | B : (string -> 'a) -> 'a t

let f (type a) (gadt: a t): a Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
       | A (ok, _) -> Ok (ok response)
       | B f -> f response)

Answer 1

您必须为每个类型变量创建一个本地抽象类型以扩展其范围，例如，以下类型检查，

let f (type ok err) (gadt: (ok,err) result t): (ok,err) result Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, _) -> Ok (ok response))

在您的示例中，您将 a 与 ('ok,'err) result 绑定在一起，编译器假设 a 是局部抽象的，那么 far-fetching 'ok 和 'err 也是抽象的。也就是说，不能用一个变量抽象出两个变量。

另外，与作用域问题无关，将'a t中的'a抽象为a，然后通过[=23]与_ result统一=] 你破坏了 a.

的抽象

let f (type a) (gadt: a t): a Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, err) ->
        Ok (ok response))

您决定忽略的错误消息表明了这一点，

Type ('a, 'b) result is not compatible with type a

'a t 的类型变量在 GADT 的所有分支中共享，并且在分支 A 到 ('ok,'error) result 中受到限制的事实并不意味着 'a t 约束到它，即使此时你的类型定义只有一个分支。

就其价值而言，虽然您的示例可能只是为了突出问题而进行的最小化，但是可以使用简单的 ADT 在没有任何 GADT 和范围问题的情况下实现相同的行为，例如，

  type 'a t = {
    ok : string -> 'ok;
    err : string -> 'err;
  } constraint 'a = ('ok,'err) result

  let f {ok; err} =
    Future.bind (fetch ()) (fun response ->
        Ok (ok response))

Answer 2

在这种情况下，另一种看待问题的方法是

let f (type a) (gadt: a t): a Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, _) -> Ok (ok response)
  )

期望类型约束 a Future.t 在正确的时间传播到 bind 函数的参数，用于将类型 ([=14=],) result 重新打包为 a.

这行不通。最小的修复是在离开模式匹配时添加注释：

let f (type a) (gadt: a t) =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, _) -> (Ok (ok response): a)
  )

通过这个注释，我们使用局部方程 ([=16=],) result=a 来确保局部类型 [=17=] 和不会逃脱它们的模式匹配分支。

当 GADT 构造函数包含多个类型变量时，局部抽象类型的范围错误

Scope error with locally abstract type when GADT constructor contains multiple type variables

types

ocaml

gadt

locally-abstract-type

完整示例

编辑：扩展示例