3 ms·

Ah I have just realized it might be "just a classic typed language IDE" experience and Dependent Types seems just way above. Am I missing something?

• namibj 7y ago
  Yes. Dependent typed tell you that the vector you pass along the matrix to a matrix-vector-multiply has to be one with not just the right datatype, but also the right size. It could also suggest (postfix w.r.t. the container type) operators with better performance for the container's known size (range). Or, depending on previous conditionals, filter postfix operators you apply to a field of a datastructure, if that field is constrained by the condition branching on another field in the datastructure. I.e., applying a specific operator to a conditional sum type that's no longer a sum type if another variable / field is restricted beyond it's datatype (a range of integers, an enum value, a theoretical utf-8 string previously restricted to ASCII, etc.).