Futhark by example (2020)(futhark-lang.org) |
Futhark by example (2020)(futhark-lang.org) |
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. 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. 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.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)
Now I'm thinking about "Smalltalk by Example" and "Slang by Example"
[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...
Futhark appears in the first paragraph! i don't think i ever read the term before
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.