5

好的，更多类型的黑客失败。:) :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 中键入级别整数）

4

1 回答 1

6

首先，您的代码中有一个真正的错误：它是let to_int = function，不是let to_int n = function。

The real problem is that you are using a polymorphic recursive function: you are calling it recursively with different types for the second parameter of the nat type. As type inference of code using polymorphic recursion is undecidable in the general case, OCaml won't try to guess it for you, so you have to be explicit with a polymorphic recursion annotation:

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

Another point that is not a problem right now but may become one in the future (and show that you still need a bit of training with GADTs): the fact that 'a s and z are distinct types is essential to your function working as you want. It tells you that if you have a value of type ('a, z) nat (note that the 'a parameter is useless in all this stuff), it can only be a Zero. You can write the following functions and they're total, you get no exhaustivity warning:

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 *)

If there was a possibility that the types z and 'a s overlap (for example if you define type 'a s = z), the type-checker could not reason on these cases being distinct, and you would have to handle the cases that I have omitted here.

The problem with your current definition is that the types 'a s and z are abstracted through a module interface. Inside the definition of the module, the definitions (as distinct abstract types) are visible, but outside the module you don't know anymore how they've been defined, and in fact maybe it was type 'a s = z. So when you are outside the module, you also won't be able to write those functions anymore. The solution is to pick concrete definitions for those types, and let them be visible through the module interface, so that the type-checker always know that they don't overlap:

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

It doesn't matter that you will never use those Z and S constructors, they're just here to let the type-checker know that z is never equal to 'a s. One could have used int and bool instead.

于 2013-03-30T18:12:55.757 回答