> For example, your invariant might be something like I’m expecting here a monotonically increasing array of numbers with a mean value of such and such and a standard deviation of such and such. The best any static type checking will let you do is “array[float]”.
Isn't this just plainly false? With dependent type system wouldn't you be able to encode all such invariants into the types? Curry-Howard isomorphism and so on?
I think so. Using existential types, we can encode predicates in such a way that the type is inhabited (i.e. there is a value of that type) only if the predicate is true.
I am learning Forth and Idris in my spare time these days. I have tried writing merge of two sorted lists in Idris, with the constraint that the merged list must have the length equal to the sum of the lengths of the input lists etc.
- frankly, I much prefer Forth :D
This is possible to do without dependent types. You could have something like this (using TS syntax):
function produceComplexArray(arr: array<number>): ComplexArray | null {
...
}
function consumeComplexArray(arr: ComplexArray) {
...
}
If the only place where you can produce a ComplexArray is produceComplexArray, and produceComplexArray ensures that the arrays it receives are "a monotonically increasing array of numbers with a mean value of such and such and a standard deviation of such and such", then all the functions after produceComplexArray can be assured that they have the right array. Therefore, even with a relatively simple type system, you can ensure this invariant.
I suspect the problem is the types begin to get fairly heavy weight. It can also start requiring you to make many atomic operations so that your invariant holds across larger chunks of code. And, that often isn't easy or really necessary.
Isn't this just plainly false? With dependent type system wouldn't you be able to encode all such invariants into the types? Curry-Howard isomorphism and so on?