存在量化的类型参数、递归函数和类型错误

Question

考虑以下 OCaml 代码：

type mytype = My : 'a list * 'a -> mytype

let rec foo : int -> mytype =
    fun n -> if n < 0 then My([], 2)
        else let My(xs, y) = foo (n - 1)
        in My(3::xs, y)

OCaml 解释器在foo 的最后一行给我一个错误， 说：

这个表达式的类型是 a#1 列表，但是一个表达式是 预期类型为 int 列表

a#1 类型与 int 类型不兼容

我可以通过将类型参数添加到 mytype 来使该代码工作，这样就可以了

type _ mytype = My : 'a list * 'a -> 'a mytype
let rec foo : int -> 'a mytype =
...

但是假设我真的不想更改mytype 的定义。然后我可以写foo，假设我想保留该函数（非工作代码直观地理解）的行为吗？

另外，有人可以解释问题的根源是什么，即为什么初始代码不进行类型检查？

Answer 1

当对mytype 值进行模式匹配时，无法知道里面是什么类型。问题是，打字系统的行为非常简单，即使 mytype 来自递归调用，它也不会尝试知道它来自哪里（打字系统不能那样工作）。

问题是，在这种情况下，您知道'a 确实是int，但您需要向编译器提供证明。

在这种特定情况下，您不需要这样做。您只需要在函数结束时使用 GADT：

let foo n =
 let rec aux n =
  if n < 0 then ([], 2)
  else let (xs, y) = aux (n - 1)
   in (3::xs, y)
 in
 let (xs,y) = aux n in My (xs,y)

值得注意的是，使用该类型定义，您无法使用您知道mytype 中有整数值的事实，因此它将非常不可用。 GADT 应该只在特定情况下使用，并且您应该准确地知道为什么以及如何使用它们。

编辑：

可以将类型视为附加到每个值的逻辑公式。在大多数情况下，它非常简单，您不必担心，主要是因为类型变量（'a'b 等等）是普遍量化的并且总是对外可见类型。

type 'a mylist = Cons of 'a * 'a list | Nil
(* should be read as:
    for all 'a,
    'a mylist is either
      * a cons containing the same 'a and 'a list
      * nil *)

type mylist = Cons : 'a * mylist -> mylist | Nil : mylist
(* should be read as:
    mylist is either
     * for some 'a, a 'a and another list
     * nil *)

在上面的 GADT 中，您可以看到没有任何内容表明列表中的每个元素都属于同一类型。事实上，如果你得到一个mylist，你就无法知道里面是什么元素。

所以，你需要证明它。这样做的一个好方法是在 gadt 中存储类型证明：

type _ proof =
 | Int : int proof
 | Float : float proof
 | Tuple : 'a proof * 'b proof -> ('a * 'b) proof
 (* You can add other constructors depending on
    the types you want to store *)

type mytype = My : 'a proof * 'a list * 'a -> mytype

现在有了这个，当打开一个mytype时，你可以匹配证明来证明'a的值。编译器会知道它是相同的，因为它会拒绝在没有与正确类型对应的证明的情况下创建 mytype。

如您所见，GADT 并不简单，在实施之前您经常需要做几个草稿。大多数情况下，您可以避免使用它们（如果您不确定它们的工作原理，请不要使用它们）。