Using type-level arithmetic in OCaml, it's easy to define a function which takes a nat higher than a specific value:
let f : 'a succ nat -> string = function _ -> "hej"
f Zero (* <-- Won't compile, argument must be > 0 *)
Is there any way to make the function accept "at most" a value, or an interval, like 0 < n < 10?
Btw, this is the type definitions:
type z = Z
type 'n succ = S of 'n
type ( 'n) nat =
| Zero : ( z) nat
| Succ : ( 'n) nat -> ( 'n succ) nat
One possibility is to use polymorphic variants.
It's definitely not beautiful like your example, though it is fairly flexible if you can stand the syntactic burden.