logoalt Hacker News

codebjelast Monday at 3:09 AM1 replyview on HN

Not for matrix multiplication, because there's no term-level chicanery to worry about; you just need phantom types for the two dimensions on your matrix type.

You can express a lot just carrying phantom types around and using basic pattern matching: in Rust I can express multiplication, concatenation of vectors to matrices, and inverses of square matrices, using phantom types.

But I can't say this, or anything remotely like it:

    struct Matrix<M: u32, N: u32, T> {
        dim: (M, N),
        // imaginary dependently typed vectors
        cells: Vec<M, Vec<N, T>>,
    }
   
    impl<M, N, T> Matrix<M, N, T> {
        fn mul<O: u32>(&self, &other: Matrix<N, O, T>) -> Matrix<M, O, T> {
            let cells: Vec<self.m, Vec<other.o, T>> = do_the_thing();
            Matrix {
                // any other values in dim, or a different type in cells, would be a type error
                dim: (self.m, other.o),
                cells
            }
        }
    }
In other words, there's no dependent pair construction without dependent types. (Or at least dependent kinds and some tricks.)

Replies

hmrylast Monday at 7:50 AM

Are M and N supposed to be type parameters in your example? If so, then you don't need to store them in the struct. And once you remove that (and switch from dynamically sized vectors to statically sized arrays) your example becomes perfectly representable in Rust and C++ without dependent types

show 1 reply