Channels

#mathematics

Title

# mathematics

b

breandan

01/24/2019, 11:44 PMThink 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 PMI 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 PMWorking 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 PMIt 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 PMMaybe there is a way to achieve #2 with

Copy code

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

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

altavir

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

b

breandan

01/26/2019, 6:42 PMIt 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 PMI 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 PMI don't see how to disambiguate a flattened array of type

`MxN`

vs `NxM`

if you don't have type level integersHow can you access an

`Int`

value to get type checked axes at compile time?a

altavir

01/26/2019, 6:45 PMIf 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 PMAt 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 PMAh, I did not understand that you need compile time check. Why would you need it?

b

breandan

01/26/2019, 6:48 PMYou don't really, I just think it's cool

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

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

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 PMThere 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 PMI 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 PMOnly 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 PMMaybe, but there is a way using

`vararg`

if you don't care about type-safe constructionBasically you assume that the user constructs the tensor correctly

a

altavir

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

b

breandan

01/26/2019, 6:55 PMthen 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 PMHere 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

b

breandan

01/26/2019, 9:16 PMInteresting, 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 PMThere was a discussion about using physical measurement units as types. It is similar.

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

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 PMFWIW 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 AMThe 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 PMMaybe 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 PMI 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