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？尝试制作添加两个不同Nat：的函数时也会发生此问题。

感谢您的帮助。

Answer 1

类型int -> 'n nat，意味着forall n, int -> n nat：该函数的用户可以选择在该n使用该函数。因此，您可以拨打of_int函数说：“嘿，这次给我一个(z s) nat”，就像您可以选择哪种类型的[] : 'a list最终结果一样。这与实际发生的不匹配，这是你不选择类型，它是由整数值决定的。

根据定义，类型系统不知道整数的值，所以您不能准确地说出您将得到哪种类型的结果为n nat。所有你可以说的是，有存在某些类型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类型（这实际上只是作为一个类型级证人很有用），所以也许有更好的方法。