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

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,说:

此表达式具有类型#1列表,但是期望类型为int list的表达式

类型#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

现在有了这个,当打开a时mytype,你可以匹配证明来证明'a'的价值.编译器会知道它是相同的,因为如果没有对应于正确类型的证明,它将拒绝创建mytype.

如您所见,GADT并不简单,在开始实施之前,您经常需要做几次草稿.大多数情况下,您可以避免使用它们(如果您不确定它们是如何工作的,请不要使用它们).