Type level encoding of natural numbers in F#

Question

I was trying to encode the natural numbers as a type in F# to be able to check an equality at compile-time instead of run-time. The best I could come up with was

type Nat<'T> =
    abstract member AsInt : int

type Z() = 
    interface Nat<Z> with 
        member __.AsInt = 0

type S<'P>(prev : Nat<'P>) =
    interface Nat<S<'P>> with 
        member __.AsInt = 1 + prev.AsInt

type TNat =
    static member zero = Z() :> Nat<Z>
    static member succ (prev : Nat<'P>) = S(prev) :> Nat<S<'P>> 
    static member one = TNat.succ(TNat.zero)
    static member two = TNat.succ(TNat.one)

I'm not sure if I'm happy with the code. Can it be done in a better (or easier) way that I am overlooking?

And can I ensure that AsInt is calculated at compile time?

Answer 1

In your code, if you try:

TNat.two = TNat.succ(TNat.one)

will yield false.

Here's an alternative implementation without interfaces:

type Z = Z with
    static member (!!) Z = 0     

type S<'a> = S of 'a with
    static member inline (!!)  (S a) = !!a + 1

let inline asInt x = !! x

let one = S Z
let two = S one

By using Discriminated Unions you benefit of structural equality as well, so in this solution you have both type (at compile time) and value (at run time) equality.

By using inline, the method to be called will be resolved at compile time.