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)