3

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
4

2 に答える 2