The advantage of dependent typing systems is that you can say that the arguments to a matrix multiplication function must have dimensions (m, i) and (i, n) and that result will have dimensions (m, n).

▲ akst 4 days ago | parent | next [-]

As others have said, this isn't a unique value proposition of dependent types, by all means dependent types provide a solution to this, but so do many other approaches.

You can do this in C++ & Rust, and I've done something similar in Typescript. The point of the comment you're replying to is kind of making the point that pitches for dependent types probably should give examples of something not already solved by other systems (not that you can't do this in DT). See:

> Yeah, this seems like matrixes might not be a great first example for explaining the value of dependent types.

In order to adopt DT, you need to pay a combined cost of productivity loss in terms of established tooling and choose to forgo any human capital which is no longer applicable once you start using a language with Dependent types, and a loss of time spent learning to use a language that has dependent types, which almost certainly has a smaller library ecosystem than most mainstream languages without DT.

For that reason it's worth considering what examples illustrate a benefit that outweighs all the above costs. I don't think it's enough to simply assert some moral basis on safety when clearly salaries for work done in unsafe languages are already considerably high.

▲

saghm 4 days ago | parent [-]

Yeah, right now there isn't really any example of the value tradeoff being high enough that its overcome the barriers to adoption. Examples making the benefits more clear are helpful in being able to talk about dependent types in my opinion because most programmers (including myself beyond a fairly surface-level understanding, honestly) probably aren't familiar with them; once that's been established, I think it's a lot easier to talk about why the approach hasn't yet become mainstream.

For example, with the potential utility in having dependent types for list APIs, the barrier is that in practice, it's not always straightforward to be able to define your code in a way where you actually know the size of the list. If I read input from a user, I might be able to do an initial check that a list of items is non-empty as part of the constructor for the type, but what happens if I want to start popping off elements from it? In practice, this seems like it would either force you to go back to manually checking or only ever process things in a purely functional way to avoid defining behavior that vary based on state that isn't known. If you're willing to take this approach, having the compiler enforce it is great! You have to be willing to use this approach often enough for it to be worth picking a language with dependent types though, and in practice it doesn't seem likely that people would choose to even if they were more aware of the option.

▲

akst 4 days ago | parent [-]

> Examples making the benefits more clear are helpful in being able to talk about dependent types in my opinion because most programmers (including myself beyond a fairly surface-level understanding, honestly) probably aren't familiar with them

There's probably some truth in that (I'm probably in this camp as well), though I feel sometimes adoption of things like this can often be a communication problem, and the people who understand these technologies the most may struggle to identify what aspect of these technologies are valued more by the people they are trying to pitch them too.

Like they might even find those aspects boring and uninteresting because they are so deep into the technology, that they don't even think to emphasis them. Which feels like a similar story where a technology early to the party didn't take off until someone else came back to them later (like fat structs and data oritented design gaining some interest despite early versions of these ideas date back to Sketchpad (1963)).

> For example, with the potential utility in having dependent types for list APIs, the barrier is that in practice, it's not always straightforward to be able to define your code in a way where you actually know the size of the list

Yeah this example crossed my mind as well, it's not immediately clear how you deal with IO or data the result of inputs from the outside world. Although I have feeling this has to be a solved problem.

I guess more generally with API design, sometimes you don't really know the system you want to model yet so there's diminishing returns in being overly precise in how you model it if those things are subject to change. Not sure how substantive a concern this is when weighing up using dependent types, but it is something that crosses my mind as an outsider to all this dependent type stuff.

▲

marklemay 4 days ago | parent [-]

The io issue can be solved in 2 ways: * by returning the pair of the list and it's length. * having functions that convert between simply typed and dependently typed lists.

However the ergonomics could probably be improved.

The API design is a real real issue, which is why I think something more "gradual" would be best.

	▲	akst 3 days ago \| parent [-]
		I haven’t entirely followed what you meant by a solution to IO, but I’m not to surprising to hear there’s a solution. I guess the point I had in mind was, in making the case of dependent languages stuff like this may not be immediately apparent (I might be confusing the concept of total languages or programming which may not necessarily be coupled to dependent types). > as an aside by IO I do mean anything not known at compile time (interrupts & user input, network responses, network requests [who API may change in a breaking way], database entries, etc) Cheers for your insight btw

▲ eru 4 days ago | parent | prev [-]

You don't need dependent types for that, either.

▲ codebje 4 days ago | parent [-]

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.