为什么 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 '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 (type a) (x : a nat) : int =
    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: 'a. 'a nat -> int = fun (type a) (x : a nat) ->
    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:polymorphic-locally-abstract。