https://kotlinlang.org logo
Channels
Powered by
#mathematics
Title
# mathematics
b

breandan

01/24/2019, 11:44 PM
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
a

altavir

01/25/2019, 3:52 PM
I really do NOT like this syntax. It it confusing and does not improve readability. The variant like
Copy code
Matrix.square(
  1.0, 0.0,
  0.0, 1.0
)
or
Copy code
Matrix.builder(2,3).build(
  1.0, 0.0, 1.0,
  0.0, 1.0, 0.0
)
Are much more concise.
Also if you want to make a lot of operations on matrices of the same dimension, you can use a builder as context.
👍 1
b

breandan

01/26/2019, 6:38 PM
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
a

altavir

01/26/2019, 6:39 PM
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.
b

breandan

01/26/2019, 6:40 PM
Maybe there is a way to achieve #2 with
Copy code
Matrix.builder(`2`, `3`)...
and then return a generically typed matrix. I'll try it
a

altavir

01/26/2019, 6:41 PM
I do not like to use numbers as variable names.
b

breandan

01/26/2019, 6:42 PM
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
a

altavir

01/26/2019, 6:42 PM
I see no problem here. I'll add the builder to kmath. Maybe tomorrow morning if I can't do it today.
b

breandan

01/26/2019, 6:44 PM
I don't see how to disambiguate a flattened array of type 
MxN
vs 
NxM
if you don't have type level integers
How can you access an 
Int
value to get type checked axes at compile time?
a

altavir

01/26/2019, 6:45 PM
If you provide explicit dimensions to builder, the builder itself knows it and uses to interpret the flat buffer dimension
b

breandan

01/26/2019, 6:47 PM
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
a

altavir

01/26/2019, 6:47 PM
Ah, I did not understand that you need compile time check. Why would you need it?
b

breandan

01/26/2019, 6:48 PM
You don't really, I just think it's cool
With type inference, you can check other arithmetic operations as well
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
a

altavir

01/26/2019, 6:50 PM
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.
b

breandan

01/26/2019, 6:51 PM
I think there might be a way to achieve it without much extra complexity
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.
a

altavir

01/26/2019, 6:53 PM
Only if you have very limited number of types like matrices up to 3x3. Otherwise it would bring combinatorial explosion
b

breandan

01/26/2019, 6:53 PM
Maybe, but there is a way using 
vararg
if you don't care about type-safe construction
Basically you assume that the user constructs the tensor correctly
a

altavir

01/26/2019, 6:54 PM
It is very simple with runtime size check. But compile-time type safety is really complicated.
b

breandan

01/26/2019, 6:55 PM
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
I need to go, I'll write about it some more later
Thanks for your feedback
a

altavir

01/26/2019, 7:07 PM
b

breandan

01/26/2019, 9:16 PM
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
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?
a

altavir

01/27/2019, 7:36 PM
There was a discussion about using physical measurement units as types. It is similar.
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.
b

breandan

02/06/2019, 11:45 PM
FWIW there is some interest in seeing this feature: https://twitter.com/breandan/status/1089715642280919042
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
a

altavir

02/07/2019, 5:16 AM
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.
b

breandan

02/07/2019, 4:19 PM
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)
a

altavir

02/07/2019, 4:31 PM
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.
2 Views
Powered by