Fsharpplus: Are nat-dependent types possible?

[nasosev]

I am writing a matrix type and a matrix multiplication function. What I would like is to have types Matrix<n,m> indexed by positive integers n, m so that the multiplication has signature

Matrix<n,m> -> Matrix<m,p> -> Matrix<n,p>

(so trying to multiply matrices of incompatible dimensions is a type error).

I have seen an implementation of this in F# (https://www.youtube.com/watch?v=3zdlQ_HjKl4 ) but the approach is quite hacky... Is it possible to do this neatly with F#+?

[gusty]

I had a quick look at that implementation.
It seems to me that it uses type providers, which should be a clean way to go.
Have you tried it? If so, which part is the hacky part? (at user level)

[nasosev]

I have not tried using it, but looking at the source, the type definitions seem quite strange, eg.

type Matrix<'t, 'd10,'d9, 'd8, 'd7, 'd6, 'd5, 'd4, 'd3, 'd2, 'd1, 'e10,'e9, 'e8, 'e7, 'e6, 'e5, 'e4, 'e3, 'e2, 'e1 when 'd10 :> Base10Digit and 'd9 :> Base10Digit and 'd8 :> Base10Digit and 'd7 :> Base10Digit and 'd6 :> Base10Digit and 'd5 :> Base10Digit and 'd4 :> Base10Digit and 'd3 :> Base10Digit and 'd2 :> Base10Digit and 'd1 :> Base10Digit and 'e10 :> Base10Digit and 'e9 :> Base10Digit and 'e8 :> Base10Digit and 'e7 :> Base10Digit and 'e6 :> Base10Digit and 'e5 :> Base10Digit and 'e4 :> Base10Digit and 'e3 :> Base10Digit and 'e2 :> Base10Digit and 'e1 :> Base10Digit and 't : struct and 't: (new: unit -> 't) and 't:> ValueType and 't :> IEquatable<'t> and 't :> IFormattable>(dim0: N10<'d10, 'd9, 'd8, 'd7, 'd6, 'd5, 'd4, 'd3, 'd2, 'd1>, dim1:N10<'e10, 'e9, 'e8, 'e7, 'e6, 'e5, 'e4, 'e3, 'e2, 'e1>, items:'t[,]) = ...
(https://github.com/allisterb/Sylvester/blob/master/src/Base/Sylvester.Tensors/Matrix.fs)

It would be nice to define the Matrix type as simply Matrix<'t,n,m>, i.e. without the base-10 expansion of the numbers.

[gusty]

Oh, I see.
So it's not that clean, in that it has a limit of 100000000 dimensions.

We could use Peano numbers, but I didn't find a way to encode them with type providers, although I'm not a skilled type provider developer.

Units of measure could be another way to explore.

[nasosev]

The "Live Checking Tooling" of the TensorFlow API for F# (https://github.com/fsprojects/fsharp-ai-tools) may be another approach but they also describe it as a hack which uses an external tool: "Build the VS tooling with the extensibility "hack" to allow 3rd party tools to add checking and tooltips".

[gusty]

Well, if it requires 3rd party extensions we can rule it out, as this is a base library.

I think in the video he mentions that Peano numbers would kill the compiler. That's certainly true if you use big numbers, for for tiny ones maybe it's not a concern.

So it seems to me that he did that hack in order to make it usable for big numbers, it's a compromise, because that hack seems to leak to the end user.

[cannorin]

I had once written type-level peano naturals with TP support and a fixed-size vector type with them https://github.com/cannorin/FSharp.Dependent

[gusty]

@cannorin That looks interesting.
@nasosev How are you planning to use this? Are you going to use big dimensions?

[nasosev]

@gusty it is for an experimental topology library, dimensions not more than 100. But I think even this limited dependent typing could be very widely applicable.

[gusty]

I agree, I have no doubt that it's very useful.
In my mind I can't think of a Vector or matrix type without this.
I'm just worried about the compiler performance. But we should definitely give it a try.
It looks like @cannorin implementation is a good place to start with.

[cannorin]

I think I can help with this (once #174 is done)

[jbotto94]

I think in the video he mentions that Peano numbers would kill the compiler. That's certainly true if you use big numbers, for for tiny ones maybe it's not a concern.

Why not use a more efficient representation of natural numbers?
Representing strictly natural numbers as binary trees is far more efficient: N = I (N) | O (N) | H.
H is 1, and you can add least significant digits, I being 1 and O being 0.
Numbers are encoded in reverse binary.

For example:

• 2 would be: OH (2 is 10 in binary)
• 5 would be HON (5 is 101 etc...).

Arithmetic operations can be implemented more efficiently.
I think this has serious benefits in terms of speed, memory and efficiency compared to the Peano numbers.

[cannorin]

Well, such kind of representations might seem more efficient, but they tend to introduce far more complicated constraints needed to be solved by the compiler than peano numbers. This is why nearly all of the existing type level programming libraries (such as GHC.TypeLits) are using peano numbers.

[cannorin]

@nasosev @gusty do you think we need to support unknown (only known at runtime) type-level naturals e.g. SomeNat :: KnownNat n => Proxy n -> SomeNat in GHC.TypeLits? The implementation strategy would be very different depending on this.

[gusty]

I was thinking only in known at compile-time, but can you exemplify in which scenario they would be useful?

[cannorin]

I'm thinking of the case when we want to use user's input value as the dimension of matrix.

[gusty]

I see.
I would rule it out for now as it might be too much :)
I have the impressions that I would complicate more than what it would help.
But that's just my opinion.

[cannorin]

Okay, I'll stick to compile-time ones for now.

[nasosev]

@cannorin @gusty For my use case, in principle all data can be known at compile-time, but I’m unsure if a compile-time solution can be effective. E.g. the kernel function for matrices has type Ker : Matrix<m,n> -> Matrix<m, a>, where a is the nullity of the matrix--a number that must be computed at runtime.
I agree that a compile-time solution is still interesting.

[cannorin]

@nasosev Matrix<m, n> -> Vector<m> list is not enough?

[nasosev]

@cannorin you are right, in many cases Matrix<m, n> -> Vector<m> list would be enough.

[cannorin]

Implementation started at https://github.com/cannorin/FSharpPlus/tree/nat-dependent-types/ .

[cannorin]

@nasosev I would really appreciate it if you could give me some advice on #201 :pray:

[cannorin]

Progress report:

[wallymathieu]

Looks sweet 😃

[cannorin]

So, I was able to create another version which takes tuple as argument and infers the dimension.

Which do you think looks better?

[gusty]

That's great. To me the tuple version looks much better and flexible.

[gusty]

Also, note that you might be able to switch curried and tupled with uncurryM and curryM ;)