Remix.run Logo
codebje 4 days ago

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.)
hmry 4 days ago | parent [-]

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

codebje 4 days ago | parent [-]

That's the "carry phantom types around" option, but it only gets you so far. If you never need to compute with the term, it's enough (see https://play.rust-lang.org/?version=stable&mode=debug&editio...).

You could use statically sized arrays, but if you can't have the static sizes of the arrays as your type parameters, but instead some arbitrary M and N, the size of your data structure isn't part of your type and you don't get the statically verified safety benefits. You also can't express M + N or anything of the sort.

Neither C++ nor Rust really hurt for expressivity, though.