Type-level arithmetic: "at most" nat or nat interval

Question

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

Answer 1

One possibility is to use polymorphic variants.

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

It's definitely not beautiful like your example, though it is fairly flexible if you can stand the syntactic burden.

Answer 2

How about the following?

By using open polymorphic variants we can write a function that can only be applied on 1,3 and 4. It would obviously be quite unwieldy to write constraints for very large numbers.

First, let's define our nat type and the numbers one to five:

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

Now let's define some types for representing our restrictions:

# 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 ]

Using these types we can express a number that is 1,3 or 4 as (last yes no yes no) nat. Here no means don't allow this number, whilst yes and last mean do allow this number. Note that we are counting from the right-hand side.

Now we can define our function. Note that we only need to include cases for the numbers in our function's domain:

# 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>

Finally, we can try out our function on the numbers one to five, getting some nice large error messages for incorrect usage:

# 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