类型级算术：“最多”nat或nat间隔

Question

使用OCaml中的类型级算法，很容易定义一个比特定值更高的nat函数：

let f : 'a succ nat -> string = function _ -> "hej"
f Zero (* <-- Won't compile, argument must be > 0 *)

是否有任何方法使函数接受“最多”一个值或间隔，如0

顺便说一句，这是类型定义：

type z = Z
type 'n succ = S of 'n
type ( 'n) nat = 
  | Zero : ( z) nat
  | Succ : ( 'n) nat -> ( 'n succ) nat

Answer 1

一种可能是使用多态变体。

let g : [`A0 of z nat | `A1 of (z succ) nat ] -> string = function
  _ -> "hej"

它肯定不像你的例子那样漂亮，尽管如果你能承受语法负担的话，它是相当灵活的。

Answer 2

下面这个怎么样？

通过使用开放的多态变体，我们可以编写一个只适用于1,3和4的函数。显然，对于非常大的数字编写约束是非常困难的。

首先，让我们定义我们的nat类型和数字1到5：

# type _ nat =
    Zero : [> `Zero] nat
  | Succ : 'a nat -> [> `Succ of 'a] nat;;
type _ nat = Zero : [> `Zero ] nat | Succ : 'a nat -> [> `Succ of 'a ] nat

# let one = Succ Zero;;
val one : [> `Succ of [> `Zero ] ] nat = Succ Zero

# let two = Succ one;;
val two : [> `Succ of [> `Succ of [> `Zero ] ] ] nat = Succ (Succ Zero)

# let three = Succ two;;
val three : [> `Succ of [> `Succ of [> `Succ of [> `Zero ] ] ] ] nat =
  Succ (Succ (Succ Zero))

# let four = Succ three;;
val four :
  [> `Succ of [> `Succ of [> `Succ of [> `Succ of [> `Zero ] ] ] ] ] nat =
  Succ (Succ (Succ (Succ Zero)))

# let five = Succ four;;
val five :
  [> `Succ of
       [> `Succ of [> `Succ of [> `Succ of [> `Succ of [> `Zero ] ] ] ] ] ]
  nat = Succ (Succ (Succ (Succ (Succ Zero))))

现在，让我们定义一些类型来表示我们的限制：

# type 'a no = [`Succ of 'a];;
type 'a no = [ `Succ of 'a ]

# type 'a yes = [ `Succ of 'a | `Zero ];;
type 'a yes = [ `Succ of 'a | `Zero ]

# type last = [ `Zero ];;
type last = [ `Zero ]

使用这些类型，我们可以表示一个数字，即1,3或4为(last yes no yes no) nat。这里no的意思是不允许这个数字，而yes和last的意思是确实允许这个数字。注意，我们是从右边数的。

现在我们可以定义我们的函数了。请注意，我们只需要在函数的域中包含数字的大小写：

# let f (x : (last yes no yes no) nat) = 
        match x with
        Succ Zero -> "1"
      | Succ (Succ (Succ Zero)) -> "3"
      | Succ (Succ (Succ (Succ Zero))) -> "4";;
val f : last yes no yes no nat -> string = <fun>

最后，我们可以在数字1到5上试用我们的函数，得到一些很好的错误消息，以避免错误的使用：

# f Zero;;
Characters 2-6:
  f Zero;;
    ^^^^
Error: This expression has type ([> `Zero ] as 'a) nat
       but an expression was expected of type last yes no yes no nat
       Type 'a is not compatible with type
         last yes no yes no = [ `Succ of last yes no yes ] 
       The second variant type does not allow tag(s) `Zero

# f one;;
- : string = "1"

# f two;;
Characters 2-5:
  f two;;
    ^^^
Error: This expression has type
         ([> `Succ of [> `Succ of [> `Zero ] as 'c ] as 'b ] as 'a) nat
       but an expression was expected of type last yes no yes no nat
       Type 'a is not compatible with type
         last yes no yes no = [ `Succ of last yes no yes ] 
       Type 'b is not compatible with type
         last yes no yes = [ `Succ of last yes no | `Zero ] 
       Type 'c is not compatible with type
         last yes no = [ `Succ of last yes ] 
       The second variant type does not allow tag(s) `Zero

# f three;;
- : string = "3"

# f four;;
- : string = "4"

# f five;;
Characters 2-6:
  f five;;
    ^^^^
Error: This expression has type
         ([> `Succ of
               [> `Succ of
                    [> `Succ of
                         [> `Succ of [> `Succ of [> `Zero ] ] as 'e ] as 'd ]
                    as 'c ]
               as 'b ]
          as 'a)
         nat
       but an expression was expected of type last yes no yes no nat
       Type 'a is not compatible with type
         last yes no yes no = [ `Succ of last yes no yes ] 
       Type 'b is not compatible with type
         last yes no yes = [ `Succ of last yes no | `Zero ] 
       Type 'c is not compatible with type
         last yes no = [ `Succ of last yes ] 
       Type 'd is not compatible with type
         last yes = [ `Succ of last | `Zero ] 
       Type 'e is not compatible with type last = [ `Zero ] 
       The second variant type does not allow tag(s) `Succ