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.Now I'm thinking about "Smalltalk by Example" and "Slang by Example"
For those that don't know, Futhark is comes from the first 6 letters of the runic alphabet (F, U, Þ, A, R, K)