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
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
一种可能性是使用多态变体。
let g : [`A0 of z nat | `A1 of (z succ) nat ] -> string = function
_ -> "hej"
它绝对不像你的例子那样漂亮，但如果你能承受句法负担，它是相当灵活的。