OCaml中的类型级算术

Question

好吧，更多类型的hackery失败。 :)：P

在我为期一周的追求摆脱（运行时）assert(n > 0)而不是静态检查它，我想出了这个模块：

module Nat : sig 
  type z
  type 'n s

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

  val add : ('a, 'n) nat -> ('a, 'n s) nat

end = struct          
  type z
  type 'n s
  type ('a, 'n) nat = 
          Zero : ('a, z) nat 
        | Succ : ('a, 'n) nat -> ('a, 'n s) nat 

  let add n = Succ n

  (*  
  let rec to_int n = function 
        | Succ a -> 1 + (to_int a)
        | Zero -> 0
        *)
end

这给出了Peano数字，其中数字以自己的类型编码：

# Zero;;
- : ('a, Nat.z) Nat.nat = Zero
# Succ (Zero);;
- : ('a, Nat.z Nat.s) Nat.nat = Succ Zero
# add (Succ Zero);;
- : ('_a, Nat.z Nat.s Nat.s) Nat.nat = Succ (Succ Zero) 

但是，最后一个函数to_int将无法编译：

Error: This pattern [Zero -> 0] matches values of type ('a, z) nat
   but a pattern was expected which matches values of type
     ('a, ex#0 s) nat

我认为这是因为z和s是不同的类型。是否有可能使它们成为相同的类型，并仍然将它们作为幻像类型？

（可能重复：type level integers in ocaml）

Answer 1

首先，你的代码中存在一个真正的错误：它是let to_int = function，而不是let to_int n = function。

真正的问题是你正在使用多态递归函数：你用nat类型的第二个参数以不同的类型递归地调用它。由于使用多态递归的代码类型推断在一般情况下是不可判定的，因此OCaml不会尝试为您猜测它，因此您必须明确使用多态递归注释：

let rec to_int : type n . ('a, n) nat -> int =
   ...

另一点现在不是问题，但可能会成为未来的一个问题（并表明您仍然需要对GADT进行一些培训）：'a s和z是不同类型的事实对于您的功能工作至关重要。它告诉你，如果你有一个('a, z) nat类型的值（注意'a参数在所有这些东西中没用），它只能是一个Zero。您可以编写以下函数并且它们是完整的，您没有得到详尽的警告：

let is_zero : ('a, z) nat -> unit = function
  | Zero -> ()
  (* case Succ not considered *)

let equal : type n . ('a, n) nat * ('a, n) nat -> bool = function
  | Zero, Zero -> true
  | Succ n1, Succ n2 -> equal (n1, n2)
  (* cases (Zero, SUcc _) or (Succ _, Zero) not considered *)

如果类型z和'a s有可能重叠（例如，如果你定义type 'a s = z），那么类型检查器无法推断这些情况是不同的，你必须处理我在这里省略的情况。

您当前定义的问题是类型'a s和z是通过模块接口抽象的。在模块的定义中，定义（作为不同的抽象类型）是可见的，但在模块之外，你不再知道它们是如何被定义的，事实上可能是type 'a s = z。因此，当您在模块外部时，您也将无法再编写这些功能。解决方案是选择这些类型的具体定义，并通过模块接口使它们可见，以便类型检查器始终知道它们不重叠：

module Nat : sig
  type z = Z
  type 'a s = S of 'a
  ...
end ...

你永远不会使用那些Z和S构造函数并不重要，他们只是在这里让类型检查器知道z永远不会与'a s相等。人们可以使用int和bool代替。