Think I have a way to get type-safe tensor operations up to a fixed length, but it requires code gen...

# mathematics

[breandan]

Think I have a way to get type-safe tensor operations up to a fixed length, but it requires code generation to implement in the general case: https://github.com/breandan/kotlingrad/blob/master/src/main/kotlin/edu/umontreal/kotlingrad/dependent/MatDemo.kt

[altavir]

I really do NOT like this syntax. It it confusing and does not improve readability. The variant like

Matrix.square(
  1.0, 0.0,
  0.0, 1.0
)

or

Matrix.builder(2,3).build(
  1.0, 0.0, 1.0,
  0.0, 1.0, 0.0
)

Are much more concise.

[altavir]

Also if you want to make a lot of operations on matrices of the same dimension, you can use a builder as context.

[breandan]

Working on the syntax, thanks for the feedback. I'm not sure if there is a way to implement syntax #2 in a type safe way. Right now I am using type-level integer literals as a substitute for dependent types. It seems to work well when you don't need to do arithmetic on the types themselves, i.e. just for composition / commutativity rules, and when need to compare whether two dimensions are the same type

[altavir]

It should work out of the box. I mean syntax number 2. Kotlin will infer the type from content of vararg in build. Did not check it though.

[breandan]

Maybe there is a way to achieve #2 with

Matrix.builder(`2`, `3`)...

and then return a generically typed matrix. I'll try it

[altavir]

I do not like to use numbers as variable names.

[breandan]

It refers to the type of the dimension, I don't think there is another way if you want type checked N-D array axes

[altavir]

I see no problem here. I'll add the builder to kmath. Maybe tomorrow morning if I can't do it today.

[breandan]

I don't see how to disambiguate a flattened array of type MxN vs NxM if you don't have type level integers

[breandan]

How can you access an Int value to get type checked axes at compile time?

[altavir]

If you provide explicit dimensions to builder, the builder itself knows it and uses to interpret the flat buffer dimension

[breandan]

At compile time? Check the implementation in the example I wrote above, it uses the type checker to check the inner dimensions match for matrix multiplication

[breandan]

https://github.com/breandan/kotlingrad/blob/928990f5cb54f8594da4f4af70c94ff24820fc13/src/main/kotlin/edu/umontreal/kotlingrad/dependent/Mat.kt#L48

[altavir]

Ah, I did not understand that you need compile time check. Why would you need it?

[breandan]

You don't really, I just think it's cool

[breandan]

With type inference, you can check other arithmetic operations as well

[breandan]

I wrote about it here: https://github.com/breandan/kotlingrad#shape-safety

[breandan]

There are three strategies, which have advantages and disadvantages. You can do the numpy broadcasting thing, you can report an error at runtime, or you can type check the shape so that invalid operations do not compile

[altavir]

There were several discusstions about similar things for kotlin and other languages. In theory it could be done even in statically typed language, but it introduces tremendous complexity and does not make a lot o sense.

[breandan]

I think there might be a way to achieve it without much extra complexity

[breandan]

While Kotlin lacks support for dependent types, I can emulate a limited version of them for type-safe tensor ops. But this approach has some caveats.

Most problematically, in order to instantiate a rank-R tensor, I need to define every combination of dimension up to a fixed constant C, requiring O(C^R) function declarations, which grows quickly intractable with the size and rank of the tensor. For example, I have implemented the rank-2 with C=4 case manually. I could use some form of code generation to do this, but maybe you have some ideas for how to improve the API? However once the tensor is constructed, I only need a constant number of functions to implement a fully type-checked tensor algebra.

[altavir]

Only if you have very limited number of types like matrices up to 3x3. Otherwise it would bring combinatorial explosion

[breandan]

Maybe, but there is a way using vararg if you don't care about type-safe construction

[breandan]

Basically you assume that the user constructs the tensor correctly

[altavir]

It is very simple with runtime size check. But compile-time type safety is really complicated.

[breandan]

then you implement the naturals up to a fixed constant, which is just linear: https://github.com/breandan/kotlingrad/blob/master/src/main/kotlin/edu/umontreal/kotlingrad/dependent/Dim.kt

[breandan]

I need to go, I'll write about it some more later

[breandan]

Thanks for your feedback

[altavir]

Here is the implementation for "type-unsafe" variant: https://github.com/altavir/kmath/blob/569ff6357b42fdbf90616127c59a40a7564608a5/kmath-core/src/commonTest/kotlin/scientifik/kmath/linear/MatrixTest.kt#L46

[breandan]

Interesting, thanks. If you remember where you saw those prior discussions on shape safety, can you refer me to them? I am curious if they found a solution to the construction issue in Kotlin or Java

[breandan]

Also, I am not sure where the extra complexity might come from, if implemented properly (possibly a naive view), but since the types are erased anyway, I don't think there will be a high performance overhead? Can you foresee any other major issues with this approach, besides the exponential constructors issue?

[altavir]

There was a discussion about using physical measurement units as types. It is similar.

[altavir]

Here is the Scala solution to your problem: https://jobs.zalando.com/tech/blog/scala-three-experiment/?gh_src=4n3gxh1

[altavir]

The problem with this approach is that it is academically beautiful, but useless in practice. If all your computations are known at compile time, there are a lot of ways to ensure dimension match. If you have user data, type system won't help you.

[breandan]

FWIW there is some interest in seeing this feature: https://twitter.com/breandan/status/1089715642280919042

[breandan]

It can be implemented in an way that does not force the user to adopt shape safe arrays. Also possible to construct them dynamically, so I believe it can be an optional set of API extensions

[altavir]

The question is what is the real use case for that? I can't imagine the case, where you work with matrices of different sizes and could accidentally mix them.

[breandan]

Maybe unlikely to confuse row-major or column-major notation, but it can be tricky for higher rank tensors. According to several discussions I’ve had, most people want typed axes, so if the axis for time coincidentally is the same shape as a different axis, you don’t implicitly broadcast. After a long chain of operations, it would be nice to infer the shape as well, sometimes I have trouble keeping track of this even for matrices. With shape safety, you get this for free (if you annotate the inputs)

[breandan]

https://arxiv.org/pdf/1710.06892.pdf

[altavir]

I think I read it somewhere outside of this paper. But again, I think that it is the problem for python with a lot of implicit operations. Here you just can add a dimension check before actual operation and throw it in runtime. I can't see the situation, where it could fail. If you want a check to be performed before calculations, there are also ways to do it without complicating the type system. For example lazy operations with ahead of time dimension check. It has some additional benefits as well.