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 realization here is that every one of the above dependent type examples are a constraint that can also be enforced by a smart constructor. The smart constructor pattern is roughly this:
module Foo
( Foo
, mkFoo
-- Any other functionality that Foo supplies
)
data Foo = ...
mkFoo :: FooInputs -> Maybe Foo
You can express all of the above dependent type constraints using this pattern. VecN can simply hold a vector and the length N constraint can be enforced in mkVecN. Similarly, SortedList can simple hold a list and the mkSortedList can sort its input and/or return Nothing if its input isn't sorted. The smart constructor mkFoo can contain arbitrarily complex Turing-complete constraints and return a Just whenever they're satisfied or a Nothing if they're not.
The key difference between dependent types and a smart constructor is that with dependent types the constraint is enforced at compile time and with a smart constructor it is checked at runtime. This suggests a rule of thumb for answering the question of whether you should use dependent types:
If the cost (TCO...i.e. the sum total of dev time, readability of the resulting code, and all the ongoing maintenance) of using a dependent type is less than the cost of handling the Nothing cases at runtime, then you should use a dependent type. Otherwise, you should just use a smart constructor.
The interesting thing here is that Haskell gives us a fantastic set of tools for handling runtime Nothing values. The Maybe type is has instances of Functor, Applicative, and Monad which allow us to avoid a lot of the code overhead of checking the failure cases and handling them appropriately. It is often possible to front load the checking of the constraint with a case statement near the top level:
case mkFoo inputs of
Nothing -> handleError
Just a -> handleSuccess a
Then all the rest of your code will be working with Foo, which is structurally guaranteed to have the properties you want and allows the use of simplified code that doesn't bother checking the error conditions.
My takeaway from this argument is that you should only reach for dependent types when dealing with situations where you can't front-load the error handling and the cost of having Maybe a's floating around your code exceeds the cost of the dependent type machinery.
What do you think? Am I missing something here? I'd love to see if anyone has practical examples of dependent types that can't be boiled down to this kind of smart constructor and runtime Maybe or where the cost of doing so is exceptionally high.
Comments
https://www.patreon.com/posts/when-i-learnt-55420196
https://github.com/andorp/order-taking/blob/cbb464f9a417a0218863e2ee6108cee074a0f010/src/Language/JSON/Schema.idr#L252-L263