是什么类型的逻辑迫使我对GADT函数选择有相同的返回类型？

Question

在this question中，向我解释了如何正确匹配GADT类型，以便使用通用量化的类型变量和本地抽象类型获得替代返回类型。尽管我在最初的示例中存在误解，但解释并没有表示：(1)类型系统在使用通用量化的类型变量时，似乎要求替代分支具有相同的返回类型，并且(2)对于期望的GADT返回类型结果，说明了一种将通用量化变量和局部抽象类型混合的优雅方法。

上述原问题的类型如下：

type
  liLabel_t = string        (* Instruction name (label) *)
and
  context_t = string
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 *)

在实验中，当替代方案都具有整数返回类型时，如：

let ft1:   'b 'c. ('b, 'c) liInstr_t -> 'b = function
(* *)  | LiExec n -> 2
(* *)  | LiExecTRY -> 24
(* *)  | LiLab s -> 4 
(* *)  | LiLabTRY -> 44
(* *)  | LiSeq (f, il) -> 42 
(* *)  | LiAlt (f, il) -> 51
(* *)  | LiLoop (f, il) -> 52
(* *)  | LiName (f, il, ic) -> 53
(* *)  | Err_LiInstr -> 54
(* *)  | Nil_LiInstr -> 55
      *               ;;

我收到错误：

Line 2, characters 21-22:
2 | (* *)  | LiExec n -> 2
                         ^
Error: This expression has type int but an expression was expected of type
         liLabel_t = string

当我注释掉这些期望GADT参数中包含string类型的分支时(如下所示)：

(* * )  | LiLab s -> 4 
(* *)  | LiLabTRY -> 44
( * *)

我知道错误是：

 ...
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
LiLab _
Lines 1-11, characters 45-26:
...
Error: This definition has type 'c. (int, 'c) liInstr_t -> int
       which is less general than 'b 'c. ('b, 'c) liInstr_t -> 'b

忽略非穷尽的模式匹配警告(这是由于变量被注释掉)，我们有一个不那么通用的函数类型定义。对此的解释见原问题的答案。

但是，如果所有分支都具有string类型，我们有时会得到类似的“不太一般”的错误，但主要是错误：

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

我还没有弄清楚为什么会有这样的行为，但我怀疑这些部门：

(* *)  | LiExecTRY -> "24"
(* *)  | LiLab s -> "4" 

如果可用，则强制一个人对所有变体都有一个string返回类型，而如果不使用任意类型，则可以返回它们。在我看来，在我看来，GADT中的LiLabel_t (即string)类型参数正在执行这种强制操作。但是怎么做呢？

如果在所有返回类型为整数的情况下使用本地抽象类型，如：

# let ft1: type b c. (b, c) liInstr_t -> b = function
(* *)  | LiExec n -> 2
(* *)  | LiExecTRY -> 24
...

我们得到了错误

Line 2, characters 21-22:
2 | (* *)  | LiExec n -> 2
                         ^
Error: This expression has type int but an expression was expected of type b

这与对GADT和本地抽象类型的原始问题的答案所解释的一样:抽象返回类型b是预期的，因为它从来没有通过GADT中的等式约束与更具体的类型相匹配。当我将所有返回类型(第一种除外)更改为string时，也会出现类似的错误。

我在original GADT question中有效地提出的总体问题是：

1. 在我的示例中，为什么我的所有返回类型都必须是int，或者是string (即LiLabel_t)，除非是第一个变体，然后才会因为返回类型b不那么一般而被拒绝。在类型检查器中所遵循的推理是什么？
2. 是否有一种优雅的方法将GADT函数中的通用量化类型和局部抽象类型结合起来，因为显然没有正确的语法方法。因为，如果我们试图混合通用量化的类型变量和本地抽象类型变量，我们总是会得到一个错误，例如：

。

Line 1, characters 10-14:
1 | let ft1: (type d) 'b 'c. ('b, 'c) liInstr_t -> d = function
              ^^^^
Error: Syntax error

Answer 1

问题1:您的示例可以简化为

type ('a,'b) t =
| A of 'a 
| B: (string,_) t

let error (x:('a,'b) t) : 'a= match x with
| A n -> 2
| B -> "hi"

第一个分支意味着'a = int。然后，第二个分支B具有(string,'c) t类型，这意味着('a,'b) t=(string,'c) t，因此'a = string，这是一个矛盾。实际上，只有抽象类型才能在模式匹配中具有局部方程，而'a和'b是统一类型变量。

(很难猜出在其他情况下出了什么问题，而这只是你曾经暗示过的，所以我会忽略它们。)

问题2:如果在所有分支中返回string，那么您的函数

let ok (x:('a,'b) t): 'a= match x with
| A n -> n
| B -> "hi"

通过将'a与string统一，将类型(string,'b) t -> string赋予ok，从而实现了良好的类型类型。但是，如果您要求打字机检查类型是否是多态的，它将通知您ok的类型不是多态的：

let not_polymorphic: 'a 'b. ('a,'b) t -> 'a= function
| A n -> n
| B -> "hi"

您可以在这里注意到，多态检查是在输入函数体之后进行的。因此，错误提到函数体的推断类型：

Error: This definition has type 'c. (string, 'c) t -> string
       which is less general than 'a 'b. ('a, 'b) t -> 'a

问题3.是的，这是可能的，但这是不常见的。

 let f (type d) (x:d) =
  let g : 'a 'b. ('a,'b) t -> d = fun _ -> x
 in g

大多数用例都可以通过速记语法得到更好的服务：

let f: type a b d. d -> (a,b) t -> d = fun d _ -> d

请你试着减少你的问题后，一次问一个问题好吗？当你在问题上层层提问时，很难猜出后面问题的根源问题。