9 ms·

Futhark is really such a great idea. I'm not convinced that dependent types are worth the cognitive overhead in general, but it's definitely worth it to include

Futhark is really such a great idea. I'm not convinced that dependent types are worth the cognitive overhead in general, but it's definitely worth it to include the length as part of the type information for dynamic arrays, e.g.: concat(Vec<T, n>, Vec<T, m>) -> Vec<T, n+m> matmul(Mat<T, n, m>, Mat<T, m, l>) -> Mat<T, n, l> head(Vec<T, n+1>) -> (T, Vec<T, n>) This would have saved me so much headache debugging CUDA kernels and numpy!! I wish it were a first-class feature in those frameworks, and even general-purpose languages, but alas.

VorpalWay 4mo ago
You can do this with templates in C++ and generics in Rust I'm pretty sure. I think the Eigen C++ library supports this. (I have yet to do a linear algebra heavy Rust project, so I can't speak to the options that exist there.)
- otabdeveloper4 4mo ago
  Yeah, C++ arrays are literally that.
  - deleted 4mo ago
    [deleted]
  - alpinisme 4mo ago
    Arrays are not dynamically sized though (handling runtime sizes) and don’t have efficient append/concat. The point of the dependent types is that you can have the type system track that concat creates an M+N length vector, sort preserves length (and adds a sorted guarantee that slice preserves), etc. Sure you can do a lot with templates, but that’s advanced templates not just “C++ arrays” in a throwaway “literally that” way.
- ethanlipson 4mo ago
  I'm talking about cases where the array size is not known at compile time. For example, say the user passes in a list of numbers as command line arguments. Then we have argv: Vec<String, argc> If I want to map these to ints, then I'd like a compile-time guarantee that the resulting array nums: Vec<Int, argc> is the same length as argv. Lean and Idris can do this, but AFAIK no commonly used languages can. But unlike general dependent types, these are not hard to wrap one's head around and would save a lot of frustration, in my experience.
itishappy 4mo ago
Here they are in Futhark: val concat [n] [m] 't : (xs: [n]t) -> (ys: [m]t) -> *[n + m]t val matmul [n] [m] [l] 't : (xs: [n][m]t) -> (ys: [m][l]t) -> *[n][l]t val head [n] 't : (x: [n]t) -> t And here's the pathological case (length cannot be determined at compile time): val filter [n] 'a : (p: a -> bool) -> (as: [n]a) -> *[]a Other pathological cases include conditionals and loops.
ainch 4mo ago
The Pyrefly type checker is starting to work on this kind of shape hinting - so far it only works on Torch but I believe the plan is for it to work with other array packages (eg. JAX, NumPy) https://pyrefly.org/en/docs/tensor-shapes/#how-it-works https://pyrefly.org/en/docs/tensor-shapes/#how-it-works
- mathisfun123 4mo ago
  Shape functions and shape analysis are basically mundane infra in almost every ML compiler/language/DSL. https://mlir.llvm.org/docs/Dialects/ShapeDialect/ https://mlir.llvm.org/docs/Dialects/ShapeDialect/
  - ainch 4mo ago
    I didn't know that, thanks for sharing. It makes sense, but then it also makes me wonder why none of the deep learning libraries (Torch, Jax/NNX, Eigen etc...) make this information available. Instead, ML people all have their own schemes for tracking shape information, like commenting '# (b, n, t)' on every line, or suffixing shapes to variable names - and in my experience it's a common source of bugs.
    - mathisfun123 4mo ago
      > Torch, Jax Both of these "make it available". Just because people don't know how to use/find them doesn't mean they're not "available". > Eigen This is not an ML anything, it's a linear algebra library. > like commenting '# (b, n, t)' on every line, or suffixing shapes to variable names There's a difference between tracking shapes in the compiler and specifying shapes in the model.
      - ainch 4mo ago
        I think we're talking at cross purposes. The reason I'm excited about the Pyrefly work is that it leverages the type system to infer array shapes statically, which makes it simpler to reason about them when you're writing the code and catch bugs. The fact that people have developed these janky approaches to shape tracking suggests that there's a gap to be filled. Jax and Torch don't do that statically. They obviously have to do it at runtime, but that doesn't address this particular issue. I mention Eigen because array shape hinting is generally useful for any linalg library, not purely for ML applications.
deleted 4mo ago
[deleted]

VorpalWay 4mo ago

You can do this with templates in C++ and generics in Rust I'm pretty sure. I think the Eigen C++ library supports this. (I have yet to do a linear algebra heavy Rust project, so I can't speak to the options that exist there.)

otabdeveloper4 4mo ago
Yeah, C++ arrays are literally that.
- deleted 4mo ago
  [deleted]
- alpinisme 4mo ago
  Arrays are not dynamically sized though (handling runtime sizes) and don’t have efficient append/concat. The point of the dependent types is that you can have the type system track that concat creates an M+N length vector, sort preserves length (and adds a sorted guarantee that slice preserves), etc. Sure you can do a lot with templates, but that’s advanced templates not just “C++ arrays” in a throwaway “literally that” way.
ethanlipson 4mo ago
I'm talking about cases where the array size is not known at compile time. For example, say the user passes in a list of numbers as command line arguments. Then we have argv: Vec<String, argc> If I want to map these to ints, then I'd like a compile-time guarantee that the resulting array nums: Vec<Int, argc> is the same length as argv. Lean and Idris can do this, but AFAIK no commonly used languages can. But unlike general dependent types, these are not hard to wrap one's head around and would save a lot of frustration, in my experience.

itishappy 4mo ago

Here they are in Futhark: val concat [n] [m] 't : (xs: [n]t) -> (ys: [m]t) -> *[n + m]t val matmul [n] [m] [l] 't : (xs: [n][m]t) -> (ys: [m][l]t) -> *[n][l]t val head [n] 't : (x: [n]t) -> t And here's the pathological case (length cannot be determined at compile time): val filter [n] 'a : (p: a -> bool) -> (as: [n]a) -> *[]a Other pathological cases include conditionals and loops.

ainch 4mo ago

The Pyrefly type checker is starting to work on this kind of shape hinting - so far it only works on Torch but I believe the plan is for it to work with other array packages (eg. JAX, NumPy) https://pyrefly.org/en/docs/tensor-shapes/#how-it-works https://pyrefly.org/en/docs/tensor-shapes/#how-it-works

mathisfun123 4mo ago
Shape functions and shape analysis are basically mundane infra in almost every ML compiler/language/DSL. https://mlir.llvm.org/docs/Dialects/ShapeDialect/ https://mlir.llvm.org/docs/Dialects/ShapeDialect/
- ainch 4mo ago
  I didn't know that, thanks for sharing. It makes sense, but then it also makes me wonder why none of the deep learning libraries (Torch, Jax/NNX, Eigen etc...) make this information available. Instead, ML people all have their own schemes for tracking shape information, like commenting '# (b, n, t)' on every line, or suffixing shapes to variable names - and in my experience it's a common source of bugs.
  - mathisfun123 4mo ago
    > Torch, Jax Both of these "make it available". Just because people don't know how to use/find them doesn't mean they're not "available". > Eigen This is not an ML anything, it's a linear algebra library. > like commenting '# (b, n, t)' on every line, or suffixing shapes to variable names There's a difference between tracking shapes in the compiler and specifying shapes in the model.
    - ainch 4mo ago
      I think we're talking at cross purposes. The reason I'm excited about the Pyrefly work is that it leverages the type system to infer array shapes statically, which makes it simpler to reason about them when you're writing the code and catch bugs. The fact that people have developed these janky approaches to shape tracking suggests that there's a gap to be filled. Jax and Torch don't do that statically. They obviously have to do it at runtime, but that doesn't address this particular issue. I mention Eigen because array shape hinting is generally useful for any linalg library, not purely for ML applications.

deleted 4mo ago

[deleted]