ocaml - 为什么 OCaml 中的 Peano 数字由于范围错误而无法正常工作？

Question

我有以下用 GADT 编写的 peano 编号:

type z = Z of z

type 'a s = Z | S of 'a

type _ t = Z : z t | S : 'n t -> 'n s t

module T = struct
  type nonrec 'a t = 'a t
end

type 'a nat = 'a t

type e = T : 'n nat -> e

以下将 'a nat(或 'a t)解码为其编码的数字的函数有效:

let to_int : type n. n t -> int =
  let rec go : type n. int -> n t -> int =
   fun acc n -> match n with Z -> acc | S n -> go (acc + 1) n
  in
  fun x -> go 0 x

但如果我尝试以几乎完全相同的方式重写它:

let to_int2 (type a) (a: a nat) : int =
  let rec go (type a) (acc : int) (x : a nat) : int =
    match x with
    | Z -> acc
    | S v -> go (acc + 1) v
  in
  go 0 a

我得到一个范围错误。这两个函数有什么区别？

138 |     | S v -> go (acc + 1) v
                                ^
Error: This expression has type $0 t but an expression was expected of type
         'a
       The type constructor $0 would escape its scope

Answer 1

根本问题是多态递归，GADT 在这里是一个红鲱鱼。

如果没有明确的注释，递归函数在它们自己的定义中不是多态的。例如，以下函数的类型为 int -> int

let rec id x =
   let _discard = lazy (id 0) in
   x;;

因为id在

中不是多态的

   let _discard = lazy (id 0) in

因此 id 0 意味着 id 的类型是 int -> 'a 导致 id 具有 int -> int 类型。为了定义多态递归函数，需要添加一个显式的全量化注释

let rec id : 'a. 'a -> 'a = fun x ->
  let _discard = lazy (id 0) in
  x

通过此更改，id 恢复其预期的 'a -> 'a 类型。此要求不会随 GADT 改变。简化你的代码

let rec to_int (type a) (x : a nat) : int =
    match x with
    | Z -> 0
    | S v ->  1 + to_int v

注解 x: a nat 暗示函数 to_int 仅适用于 a nat，但您申请的是不兼容的类型(以及那些生活在一个太窄的范围内但这是次要的)。

与非 GADT 情况一样，解决方案是添加显式多态注释:

let rec to_int: 'a. 'a nat -> int = fun (type a) (x : a nat) ->
    match x with
    | Z -> 0
    | S v ->  1 + to_int v

由于形式为 'a。 'a nat -> int = fun (type a) (x : a nat) -> 是 GADT 上的递归函数经常需要的内容，有一个可用的快捷表示法:

let rec to_int: type a. a nat -> int = fun x ->
    match x with
    | Z -> 0
    | S v ->  1 + to_int v

对于不太熟悉 GADT 的人来说，这种形式是编写 GADT 函数时首选的形式。事实上，这不仅避免了多态递归的问题，而且在尝试实现函数之前写下函数的显式类型通常是 GADT 的好主意。

另见 https://ocaml.org/manual/polymorphism.html#s:polymorphic-recursion , https://ocaml.org/manual/gadts-tutorial.html#s%3Agadts-recfun , 和 https://v2.ocaml.org/manual/locallyabstract.html#p:polymorpic-locally-abstract .