Can i define type-level naturals in F#, then use them in C#?

Question

In an earlier question I wondered if there is some way in C# to implement matrix dimensionality as a type-level property. That is, I wanted to be able to declare a generic family of classes of the form Matrix<M, N>, where M and N are natural numbers. The ultimate goal was to have dimensionality checks at compile-time, so that, for example, trying to multiply a 3x3 matrix by a 2x3 matrix should yield a compile-time error, or having functions that only accept square matrices (Matrix<M, M>).

Unfortunately it does not seem like this is possible in C#, the issue being that M and N in the generic type Matrix<M, N> have to be types, not integers. Some other languages seem to have mechanisms that get around this issue however:

1. Some functional languages, such as Haskell, have the possibility to define type-level naturals. If this were possible in C#, then it should also be possible to define Matrix<M, N>, with M and N being type-level naturals. I don't know much about F#, but this answer seems to indicate that this is possible in F# as well.

2. In C++ one can use templates with non-type template parameters. If I understand it correctly, classes for the specific sizes that are actually used in the code are then generated at compile-time.

3. Haskell has something called indexed type families that seem capture exactly the concept I am after.

Now, since C# and F# are both .NET languages I am primarily interested in point 1 above. Would it perhaps be possible to implement the types that I need in F#, and then provide them to my application as a library? The best would be if I could define only the type-level naturals in F#, and then use them in C# to define Matrix<M, N>.

Answer 1

I would do this using an interface with a static member. In F#, you can define type-level natural numbers like this:

namespace TypeLevelNatural

#nowarn "3535"   // allow interfaces with static abstract members

/// Type-level interface that all natural numbers must implement.
type Natural =
    static abstract Size : int

/// Type zero.
type Zero =
    interface Natural with
        static member Size = 0

/// Type-level successor function.
type Successor<'t when 't :> Natural>() =
    interface Natural with
        static member Size = 't.Size + 1

/// Define 1, 2, 3, ...
type One() = inherit Successor<Zero>()
type Two() = inherit Successor<One>()
type Three() = inherit Successor<Two>()
type Four() = inherit Successor<Three>()

Then in C#, you can define a matrix like this:

using TypeLevelNatural;

class Matrix<NRows, NCols>
    where NRows : Natural
    where NCols : Natural
{
    public double[,] Values = new double[NRows.Size, NCols.Size];
}

Example usage:

var matrix = new Matrix<Two, Three>();

for (int iRow = 0; iRow < matrix.Values.GetLength(0); iRow++)
{
    for (int iCol = 0; iCol < matrix.Values.GetLength(1); iCol++)
        Console.Write($" {matrix.Values[iRow, iCol]}");
    Console.WriteLine();
}

Output is:

 0 0 0
 0 0 0