Dependent Types are a Runtime Maybe
Awhile back I was discussing dependent types with someone and we ended up concluding that dependent types can always be replaced by a runtime Maybe. This seemed to me then (and still does today) as a fairly surprising and provocative conclusion. So I thought I'd put the idea out there and see what people think. Let's look at a few examples that are commonly used to illustrate dependent types: Vectors of length N Matrices of size m x n Sorted lists Height-balanced trees (trees where the height of subtrees differ by at most one) The argument is roughly as follows. All of these examples ultimately boil down to enforcing some kind of constraint on some data types. The more powerful your dependent type system, the more rich and expressive will be the constraints that you can enforce. If we take this thought experiment to its logical conclusion, we end up with a dependent type system that allows us to enforce any constraint that can be computed. The important rea...