ocaml - 类型级算术 : "at most" nat or nat interval

Question

在 OCaml 中使用类型级算法，很容易定义一个函数，该函数的 nat 值高于特定值:

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

有没有办法让函数“至多”接受一个值或一个区间，比如 0 < n < 10？

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

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"

它绝对不像你的例子那么漂亮，但如果你能承受句法负担，它是相当灵活的。