types - 具有差异列表的 Nat 类型

Question

我将自然数编码为差异列表:

type z = Z
type +'a s = S

type _ nat =
  | Z : ('l * 'l) nat
  | S : ('l * 'm) nat -> ('l * 'm s) nat

这让我可以轻松地对加法进行编码:

let rec add : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat =
  fun i1 i2 ->  match i2 with
    | Z -> i1
    | S i -> S (add i1 i) (* OK *)

但是以下变体不进行类型检查:

let rec add2 : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat =
  fun i1 i2 ->  match i2 with
    | Z -> i1
    | S i -> add2 (S i1) i    (* KO *)

有没有人知道如何让它正确，即有一个高效的类型添加，可能改变 Nat 类型？

请注意，这个问题比 Nat 加法更普遍:对于更复杂的类型，同样的问题也会出现。例如。使用大小列表，所有基于累加器的函数(如 rev_append)都很难输入。

Answer 1

这里的问题是 S i1 的类型是 (l s * m s) nat 而 i 的类型是 m * n。因此，对 add2 的递归调用是错误类型的:add2 期望其第一个参数的最右边索引与其第二个参数的最左边索引匹配，并且 m s 绝对不同于 m。

因为您将一个值编码为差异，所以您可以轻松解决这个问题:您可以注意到 (l * m) nat 和 (l s * m s) nat应该是一样的东西。你确实可以定义一个函数 shift 将一个转换为另一个，这基本上是一个恒等函数:

let rec shift : type l m. (l*m) nat -> (l s * m s) nat = function
  | Z   -> Z
  | S i -> S (shift i)

然后，您可以在对 add2 的递归调用中调整 i 的类型，以对整个内容进行类型检查:

let rec add2 : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat =
  fun i1 i2 ->  match i2 with
    | Z -> i1
    | S i -> add2 (S i1) (shift i)

编辑:摆脱非尾递归 shift。

继续传递样式转换

将非尾递归函数转换为尾递归函数的常用技术是在 Continuation Passing Style 中定义它。 : 该函数带有一个额外的参数，该参数描述了如何处理返回值

我们可以将 shift 变成尾递归函数 shift3 ，如下所示:

let shift3 : type l m. (l*m) nat -> (l s * m s) nat =
  let rec aux : type l m c. ((l s * m s) nat -> c) -> (l * m) nat -> c =
   fun k i -> match i with
     | Z -> k Z
     | S j -> aux (fun i -> k (S i)) j
  in fun i -> aux (fun x -> x) i

然后让我们定义 add3:

let rec add3 : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat =
  fun i1 i2 ->  match i2 with
    | Z -> i1
    | S i -> add3 (S i1) (shift3 i)

大锤:Obj.magic

摆脱非尾递归 shift 函数的一种(简单但肮脏的)方法是用 Obj.magic 替换它:确实，如前所述，我们的 shift 只不过是结构定义的恒等函数。

这导致我们:

let shift4 : type l m. (l*m) nat -> (l s * m s) nat = Obj.magic

let rec add4 : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat =
  fun i1 i2 ->  match i2 with
    | Z -> i1
    | S i -> add4 (S i1) (shift4 i)