breandan

    breandan

    3 years ago
    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

    altavir

    3 years ago
    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.
    Also if you want to make a lot of operations on matrices of the same dimension, you can use a builder as context.
    breandan

    breandan

    3 years ago
    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

    altavir

    3 years ago
    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

    breandan

    3 years ago
    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

    altavir

    3 years ago
    I do not like to use numbers as variable names.
    breandan

    breandan

    3 years ago
    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

    altavir

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

    breandan

    3 years ago
    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?
    altavir

    altavir

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

    breandan

    3 years ago
    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
    altavir

    altavir

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

    breandan

    3 years ago
    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
    altavir

    altavir

    3 years ago
    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

    breandan

    3 years ago
    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.
    altavir

    altavir

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

    breandan

    3 years ago
    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
    altavir

    altavir

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

    breandan

    3 years ago
    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
    breandan

    breandan

    3 years ago
    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?
    altavir

    altavir

    3 years ago
    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.
    breandan

    breandan

    3 years ago
    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
    altavir

    altavir

    3 years ago
    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

    breandan

    3 years ago
    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)
    altavir

    altavir

    3 years ago
    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.