如何为GADT类型的模式匹配获取更具体的替代返回类型？

我希望利用GADT实现('a, 'b) liInstr_t类型，用于存储各类指令，这些指令可递归解码为基础操作后执行。但在模式匹配时，无法将函数参数的局部抽象类型与GADT期望的不同具体返回类型关联起来。查阅OCaml 4.10.0手册中关于locally abstract types和GADTs的内容、《Real World OCaml》及相关问题解答后仍未解决。

定义的GADT类型 #

type
  liLabel_t = string        (* Instruction name (label) *)
and
  context_t = string        (* TODO: execution context *)
and
  'a context_list_t = 'a list
and
  'a liChooser_t = 'a -> int    (* get index of i-th list entry *)
and
  ('a, 'b) liInstr_t =
    LiExec: 'a -> ('a, 'b) liInstr_t        (* executable operation *)
  | LiExecTRY: ('a, _) liInstr_t        (* Ignore: Experiment on GADT *)
  | LiLab: liLabel_t -> ('a, 'b) liInstr_t  (* instruction label *)
  | LiLabTRY: (liLabel_t, _) liInstr_t      (* Ignore: Experiment on GADT *)
  | LiSeq: 'a liChooser_t * 'b list -> ('a, 'b) liInstr_t   (* sequence *)
  | LiAlt: 'a liChooser_t * 'b list -> ('a, 'b) liInstr_t   (* choice *)
  | LiLoop: 'a liChooser_t * 'b list -> ('a, 'b) liInstr_t  (* loop *)
  | LiName: 'a liChooser_t * liLabel_t * 'b context_list_t ->
    ('a, 'b) liInstr_t              (* change context *)
  | Err_LiInstr: ('a, 'b) liInstr_t     (* error handling *)
  | Nil_LiInstr: ('a, 'b) liInstr_t     (* no action *)

出错的示例函数与错误信息 #

示例函数ft1 #

let ft1:  type  b c. (b, c) liInstr_t -> b = function
(* *)  | LiExec n -> n
(* *)  | LiExecTRY -> "4"
(* *)  | LiLab s -> "LiLab" 
(* *)  | LiLabTRY -> "LiLabTRY"
(* *)  | LiSeq (f, il) -> "LiSeq" 
(* *)  | LiAlt (f, il) -> "LiAlt" 
(* *)  | LiLoop (f, il) -> "LiLoop"
(* *)  | LiName (f, il, ic) -> "LiName"
(* *)  | Err_LiInstr -> "Err_LiInstr"
(* *)  | Nil_LiInstr -> "Nil_LiInstr"
;;

错误信息 #

Line 3, characters 22-25:
3 | (* *)  | LiExecTRY -> "4"
                          ^^^
Error: This expression has type string but an expression was expected of type
         b

问题与解答 #

问题1：如何捕获并使用模式匹配分支中的抽象类型？为何我的类型b和c未正确绑定到返回类型？如何为返回类型找到与抽象类型匹配的值？ #

• 要捕获分支中的抽象类型，必须让GADT构造器明确绑定类型参数。比如你的LiExecTRY当前定义为('a, _) liInstr_t，'a是完全多态的，没有被构造器参数约束；如果希望这个分支返回字符串，应该把它改成LiExecTRY: (string, _) liInstr_t，这样匹配到该分支时，局部抽象类型b就被固定为string，返回"4"就合法了。
• 你的b和c未正确绑定，是因为除了LiExec和LiLabTRY之外，其他构造器都没有把'a（即函数中的b）与构造器的参数或自身做类型关联。比如LiLab的类型是liLabel_t -> ('a, 'b) liInstr_t，'a不受约束，意味着它可以对应任意类型，模式匹配时无法确定b的具体类型，自然不能返回固定的字符串（因为b可能是int、float等）。
• 要让返回类型匹配抽象类型，需要让构造器携带足够的类型信息，将'a（即b）固定下来。比如如果LiLab分支要返回字符串，应将其定义为LiLab: liLabel_t -> (string, 'b) liInstr_t，这样匹配到LiLab时，b就是string，返回"LiLab"就符合类型要求。

问题2：为何所有分支必须返回相同类型（如示例中的string），而不能使用GADT支持的多种结果类型？为何抽象类型和多态变量对返回类型无影响？ #

• 所有分支必须返回相同类型，是因为你给ft1指定的返回类型是局部抽象类型b——它代表调用者可以选择的任意类型，意味着函数必须能接受任意(b,c)指令并返回b类型的值。但你的大多数构造器没有约束b的类型，无法生成符合任意b类型的值，返回固定字符串自然会报错。
• GADT支持多种结果类型的前提是，构造器要把返回类型的具体信息编码到自身类型中。比如LiExec的类型是'a -> ('a, 'b) liInstr_t，它明确将'a（即返回类型b）与构造器参数类型绑定，所以这个分支可以返回n（类型就是b）。但其他构造器没有利用GADT的特性约束类型参数，和普通代数类型没区别，自然无法实现多态返回类型。
• 抽象类型和多态变量对返回类型无影响，是因为你的GADT构造器没有发挥GADT的核心作用——为不同构造器的类型参数设置不同约束。除了LiExec和LiLabTRY，其他构造器的类型参数都是不受约束的，无法为模式匹配提供类型信息，也就无法影响返回类型。

问题3：如何混合多态类型与局部抽象类型以避免语法错误？例如尝试let ft1: (type d) 'b 'c. ('b, 'c) liInstr_t -> d = function时出现语法错误。 #

• OCaml的语法要求，局部抽象类型的声明(type ...)必须放在多态类型变量的前面，正确的写法有两种：
  1. 将局部抽象类型声明放在类型注解内部：

     let ft1 : 'b 'c. (type d) ('b, 'c) liInstr_t -> d = function
     

  2. 将局部抽象类型声明放在let绑定的类型参数部分，写法更清晰：

     let ft1 (type d) : 'b 'c. ('b, 'c) liInstr_t -> d = function
     

• 注意：这种写法本身存在逻辑问题——返回类型d是任意类型，你无法在分支中返回符合任意d类型的值（除非所有分支都返回多态值，比如()）。正确的做法是让返回类型与GADT的类型参数关联，利用GADT的类型约束实现不同分支返回不同类型的结果。

内容的提问来源于stack exchange，提问作者wss