OCaml 中的多态递归：返回值

Question

继续我关于类型级算术的一系列问题，我偶然发现了另一个问题：多态递归函数的返回类型。

这是代码：

module Nat : sig
  type z = Z
  type 'n s = S of 'n

  type ('n) nat =
          Zero : (z) nat
        | Succ : ('n) nat -> ('n s) nat

  val of_int : int -> 'n nat
end = struct
  type z = Z
  type 'n s = S of 'n
  type ( 'n) nat =
          Zero : ( z) nat
        | Succ : ('n) nat -> ('n s) nat

  let rec of_int n : int -> 'n nat = function
        0 -> Zero
        | n -> Succ (of_int (n - 1))
end

编译产量：

Error: This expression [Succ (of_int (n - 1))] has type 'a s nat
   but an expression was expected of type z nat

问题是函数的返回值在第一个模式匹配子句中被零设置为z nat。相反，它应该是类似 'a. '一个纳特？尝试制作添加两个不同 Nat:s 的函数时也会出现此问题。

感谢您的帮助。

Answer 1

类型int -> 'n nat，表示forall n, int -> n nat：函数的用户可以选择在哪个n使用该函数。所以你可以调用of_int 函数说“嘿，这次给我一个(z s) nat”，就像你可以选择[] : 'a list 最终是哪种类型一样。这和实际情况不符，就是你没有选择类型，它是由整数的值决定的。

根据定义，整数的值对于类型系统来说是未知的，所以你不能准确地说出你会得到哪个类型n nat。你能说的就是exists一些类型n，比如结果有类型n nat。您可以使用“存在类型”来表达这一点，并且有多种方法可以做到这一点，GADT 就是其中之一（GADT 是代数数据类型加上存在类型和等式约束）。

type some_nat =
| Some : 'n nat -> some_nat

let rec of_int = function
| 0 -> Some Zero
| n ->
  let (Some nat) = of_int (n - 1) in
  Some (Succ nat)

some_nat 是围绕nat 的存在包装，如果你有一流的存在类型，它相当于你可能写的exists n. n nat。

处理加法更加困难，因为您必须在类型级别表示您返回的类型确实对应于其他两种类型的加法。以下是我为它定义类型的方式：

type (_, _, _) add =
| AddZ : (z, 'b, 'b) add
| AddS : ('a, 'b, 'c) add -> ('a s, 'b, 'c s) add

type ('a, 'b) add_result =
| Result : ('a, 'b, 'c) add * 'c nat -> ('a, 'b) add_result

let rec add : type a b . a nat -> b nat -> (a, b) add_result = function
   ...

我会让你定义add 的主体，这样你就可以自己玩这些东西了。

我对围绕 add 类型的所有运行时包装不太满意（这实际上只是作为类型级见证有用），所以也许有更好的方法。