类型级 Peano 算术：类型构造函数将逃避其作用域

问题描述

我尝试在 Ocaml 中的类型级别上实现 Peano 算法，但遇到了一个问题：

module Nat = struct
  type zero = Z

  type 'a succ = S

  type 'a nat = Zero : zero nat | Succ : 'a nat -> 'a succ nat
end

现在，如果我想实现 add，关于这个操作的两个公理是：

我试过了

let rec add : type n1 n2. n1 nat -> n2 nat -> 'a nat =
  fun a b -> match b with Zero -> a | Succ b' -> Succ (add a b')

但是

9 |    fun a b -> match b with Zero -> a | Succ b' -> Succ (add a b')
                                       ^
Error: This expression has type n1 nat but an expression was expected of type
         'a nat
       The type constructor n1 would escape its scope

我也有第二个分支的错误：

let rec add : type n1 n2. n1 nat -> n2 nat -> 'a nat =
  fun a b -> match b with Succ b' -> Succ (add a b') | Zero -> a

9 |    fun a b -> match b with Succ b' -> Succ (add a b') | Zero -> a
                                               ^^^^^^^^^^
Error: This expression has type 'a succ nat
       but an expression was expected of type 'a nat
       The type variable 'a occurs inside 'a succ

如果我将 Succ 放在递归调用中：

let rec add : type n1 n2. n1 nat -> n2 nat -> 'a nat =
   fun a b -> match b with Succ b' -> add (Succ a) b' | Zero -> a

9 |    fun a b -> match b with Succ b' -> add (Succ a) b' | Zero -> a
                                                                    ^
Error: This expression has type n1 nat but an expression was expected of type
         'a nat
       The type constructor n1 would escape its scope

当我添加另一个类型变量时，错误发生了变化：

let rec add : type n1 n2 n3. n1 nat -> n2 nat -> n3 nat =
   fun a b -> match b with Succ b' -> add (Succ a) b' | Zero -> a

9 |    fun a b -> match b with Succ b' -> add (Succ a) b' | Zero -> a
                                                                    ^
Error: This expression has type n1 nat but an expression was expected of type
         n3 nat
       Type n1 is not compatible with type n3

我不习惯 GADT，所以我对如何解决这个打字问题以及是否可以解决有点迷茫。

解决方法

根本问题是函数 add 的类型不是 'a nat -> 'b nat -> 'c nat。

此外，没有这种类型的非发散值，因为返回类型 'c. 'c nat 是普遍量化的。因此，_ nat -> _ nat -> 'c nat 类型的函数有望一次返回所有整数。

add 的幻想类型类似于 'a nat -> 'b nat -> ('a + 'b) nat，其中类型表达式 ('a + 'b) 正在计算加法。但是，对于一元整数的直接编码，无法执行此计算。与一元整数的非类型表示相比，这并不完全令人惊讶

type u = Z | Succ of u

GADTs 版本更多类型化，因此与非类型化版本相比禁止某些功能。函数 add 就是这种类型错误的函数之一。

换句话说，如果我们想要一个加法函数，我们需要一种允许在类型级别执行计算 'a nat -> 'b nat -> ('a+'b) nat 的编码。此外，在 HM 类型系统中，键入时进行的唯一计算是类型变量的统一。因此，我们需要选择一种可以通过统一计算加法的编码。

幸运的是，有一种几何编码有效。考虑具有命名端点的一维向量整数向量：

0 = ||
    a b

1 = |-|
    a b

如果我想添加一个向量 u 和 v，我可以用

|-----------|-------------|
a    u     b=c      v     d

这里，我通过取u+v的左端点、u的右端点并统一v的右端点来计算向量u和 u 的左端点。换句话说，我通过统一计算了一个加法。并且该编码可以用 GADT 表示：

type ('left,'right) nat =
| Z : ('p,'p) nat
| S: ('left,'right) nat -> ('left,'right succ) nat

let rec add: type left mid right.
(left,mid) nat -> (mid,right) nat -> (left,right) nat =
fun x y -> match y with
| Z -> x
| S y -> S (add x y)

有了这个添加工作。但是，由于值限制，这种编码很难使用。特别是 add 函数返回的值不是多态的，这在我们使用统一进行类型级计算时会产生问题。

ocaml ocaml