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.
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)
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.
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.
> Jax and Torch don't do that statically. They obviously have to do it at runtime, but that doesn't address this particular issue.
You don't understand what you're talking about.
Jax is explicitly mentioned in your pyrefly link as having a parallel (but slightly weaker) system. In addition Jax is built on stablehlo which uses shape dialect, which is part of the compiler (and therefore statically known).
Torch has a symbolic shape inference system that I helped build:
> The fact that people have developed these janky approaches to shape tracking suggests that there's a gap to be filled.
I have already said it: the fact that people do not know how to use the tools does not mean the tools are lacking - it means the users are unsophisticated. Let me put it this way: almost everyone that is employed to work with these tools is aware of these features and therefore eschews those kinds of comment strings.
Thanks for the reply - you're clearly much more experienced with the internals here, but I believe we're still talking at cross-purposes. I believe you're talking about compilers like jax.jit or torch.compile performing symbolic shape inference. I'm talking about the ergonomics of tracking shape information while writing Python code that calls these libraries. I don't use Torch much, so I'll just comment on the Jax side.
> Jax is explicitly mentioned in your pyrefly link as having a parallel (but slightly weaker) system
Jaxtyping is limited to runtime-only checks (which might as well be assert statements), and doesn't infer shapes based on operations. I'm interested in Pyrefly because I've run into the limitations of Jaxtyping in my own usage.
> Jax is built on stablehlo which uses shape dialect, which is part of the compiler (and therefore statically known).
It's true that JAX does shape inference when it compiles down to HLO - but that isn't available to the Python typing system. The Pyrefly development is addressing that, so you get static analysis before even running anything, or without having to add eval_shape calls all over your codebase. I think that's helpful, and will catch bugs. When I say Jax does inference at runtime, I mean that you have to run for the jit compiler to kick in - you don't get feedback as you edit.
> the fact that people do not know how to use the tools does not mean the tools are lacking... almost everyone that is employed to work with these tools is aware of these features and therefore eschews those kinds of comment strings.
The examples I took are from Andrej Karpathy and Noam Shazeer - maybe the disconnect is that they're more on the research side. Perhaps only unsophisticated users rely on these hacks - but as one such user I'm very excited that Pyrefly is addressing a problem I have. I suspect part of the misunderstanding that's evolved here is that these tools serve audiences with different needs.
Every single comment you've posted was unhelpful and demeaning and you've constantly had to backtrack every single time you've had to respond. This is extremely poor form and I see zero goodwill here.
ainch doesn't care about the inference engine knowing the shapes. This is obvious. He has been talking about developer ergonomics and you've basically said "only idiots don't know where the ergonomics features are", while linking to a file which explicitly states that it is a experimental/private API that is only needed in niche situations which is basically doubling down on having poor ergonomics.
If you can't understand the problem as a developer working on those features and you had to link to the source you've written rather than the docs, you're basically admitting that you're the problem.
I use jaxtyping as documentation, but the fact it can only be used for runtime checking (in a slightly clunky manner) and can't infer shapes based on ops really limits its utility imo.
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.)
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.
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.
> That's like calling your programming language Latin?!
More accurately it would be like calling it Alphabet, since that takes its name from Alpha Beta (AB) just like the Futhark takes its name from the first letters in it.
Eh. Words get overloaded all the time and this is a website focusing on programming after all. Would you consider "Python by example" or "C by example" to need disambiguation because they're not about snakes or about the third letter of the alphabet?
Also the very first line on that page is "The Futhark Programming Language" so if you were still confused after that I think it's on you.
If Python were the language spoken in Fictionastan then yes, and C is indeed even more terrible than something like Golang but that predates the internet so it's pretty searchable after all
> if you were still confused after that I think it's on you
Generally the point of a title (if the domain name doesn't already do it) is to help you understand what it's about so you know whether to click. If it takes a click to read the explanation before you can know whether you're interested, all links on the HN homepage might as well have no string at all and just be "click here to find out what the link is about"
It is a pretty confusing name. Personally I'm waiting for someone to name a programming language Womble. Underground, overground, you're free to use it as long as you work as a team and are tidy and clean.
Futhark is pretty great! And I have to say that the maintainer is insanely quick. It has happened on more than one occasion that I reported a bug and it's solved within the day. I have been using Futhark in prod for two years now and never had serious problems.
It would be nice to not name your language after another language. (Yes I know it's a script, that doesn't change my point). I came here expecting something else.
Yeah, when naming your language, it's important to keep mind the expectations of people seeing headlines about articles about your language on blog aggregation sites :^)
Now I'm thinking about "Smalltalk by Example" and "Slang by Example"
Same. Thought I had a copy of Uthark [1][2] on my shelf too but alas I seem to have only retained Svartkonst [3] during the tragic downsizing of my library.
Couldn’t have chosen a more difficult (and ambiguous) name to pronounce, could you? It almost sounds like a curse that I often hear people say out in the bad streets of New York City.
Elder [0] and Younger [1] Futhark (or Fuþark) are the name of two runic writing systems used by Germanic and Scandinavian Vikings. The name Futhark is a combination of the first 6 runes /f/, /u/, /ð/, /ɑ/, /r/, and /k/. Similar to how you get the name "alphabet" from the first two letters of Greek's writing system.
https://pyrefly.org/en/docs/tensor-shapes/#how-it-works
https://mlir.llvm.org/docs/Dialects/ShapeDialect/
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.
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.
You don't understand what you're talking about.
Jax is explicitly mentioned in your pyrefly link as having a parallel (but slightly weaker) system. In addition Jax is built on stablehlo which uses shape dialect, which is part of the compiler (and therefore statically known).
Torch has a symbolic shape inference system that I helped build:
https://github.com/pytorch/pytorch/blob/main/torch/fx/experi...
> The fact that people have developed these janky approaches to shape tracking suggests that there's a gap to be filled.
I have already said it: the fact that people do not know how to use the tools does not mean the tools are lacking - it means the users are unsophisticated. Let me put it this way: almost everyone that is employed to work with these tools is aware of these features and therefore eschews those kinds of comment strings.
> Jax is explicitly mentioned in your pyrefly link as having a parallel (but slightly weaker) system
Jaxtyping is limited to runtime-only checks (which might as well be assert statements), and doesn't infer shapes based on operations. I'm interested in Pyrefly because I've run into the limitations of Jaxtyping in my own usage.
> Jax is built on stablehlo which uses shape dialect, which is part of the compiler (and therefore statically known).
It's true that JAX does shape inference when it compiles down to HLO - but that isn't available to the Python typing system. The Pyrefly development is addressing that, so you get static analysis before even running anything, or without having to add eval_shape calls all over your codebase. I think that's helpful, and will catch bugs. When I say Jax does inference at runtime, I mean that you have to run for the jit compiler to kick in - you don't get feedback as you edit.
> the fact that people do not know how to use the tools does not mean the tools are lacking... almost everyone that is employed to work with these tools is aware of these features and therefore eschews those kinds of comment strings.
The examples I took are from Andrej Karpathy and Noam Shazeer - maybe the disconnect is that they're more on the research side. Perhaps only unsophisticated users rely on these hacks - but as one such user I'm very excited that Pyrefly is addressing a problem I have. I suspect part of the misunderstanding that's evolved here is that these tools serve audiences with different needs.
ainch doesn't care about the inference engine knowing the shapes. This is obvious. He has been talking about developer ergonomics and you've basically said "only idiots don't know where the ergonomics features are", while linking to a file which explicitly states that it is a experimental/private API that is only needed in niche situations which is basically doubling down on having poor ergonomics.
If you can't understand the problem as a developer working on those features and you had to link to the source you've written rather than the docs, you're basically admitting that you're the problem.
https://docs.kidger.site/jaxtyping/
Turns out, Futhark != https://en.wikipedia.org/wiki/Futhark (runes, old germanic alphabet)
That's like calling your programming language Latin?! The title could use some disambiguation...
More accurately it would be like calling it Alphabet, since that takes its name from Alpha Beta (AB) just like the Futhark takes its name from the first letters in it.
Also the very first line on that page is "The Futhark Programming Language" so if you were still confused after that I think it's on you.
> if you were still confused after that I think it's on you
Generally the point of a title (if the domain name doesn't already do it) is to help you understand what it's about so you know whether to click. If it takes a click to read the explanation before you can know whether you're interested, all links on the HN homepage might as well have no string at all and just be "click here to find out what the link is about"
For those that don't know, Futhark is comes from the first 6 letters of the runic alphabet (F, U, Þ, A, R, K)
https://www.youtube.com/@JacksonCrawford
Now I'm thinking about "Smalltalk by Example" and "Slang by Example"
https://en.wikipedia.org/wiki/Runes#Runic_alphabets
https://en.wikipedia.org/wiki/Elder_Futhark
[1] https://archive.org/details/karlsson-thomas-uthark-nightside...
[2] https://www.84cxrarebooks.com/pages/books/090763/t-ketola-th...
[3] https://www.miskatonicbooks.com/product/thursakyngi-iv-svart...
[0]: https://en.wikipedia.org/wiki/Elder_Futhark
[1]: https://en.wikipedia.org/wiki/Younger_Futhark
Futhark appears in the first paragraph! i don't think i ever read the term before