codebje • yesterday at 3:09 AM

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.)