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是不同的类型.是否有可能使它们成为相同的类型,并仍然将它们作为幻像类型？

(可能重复: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不是.