In team software projects, significant problems are often caused by inconsistent assumptions between two or more people. We often resort to informal agreements on paper (or in email) that may or may not remain consistent with our code over time. But these specifications don’t need to be informal in the right programming environments, because types are propositions, and proofs are programs.
To what extent can this observation save us from ourselves?
From the play:
VLADIMIR: What are we doing here, that is the question. And we are blessed in this, that we happen to know the answer. Yes, in this immense confusion one thing alone is clear. We are waiting for Godot to come—
Whenever we choose a programming language to represent a plan or procedure we intend to realize, we fundamentally choose whether we prefer completeness or consistency. It’s often easier to choose completeness when there’s just one person involved, because (unless you’re Walt Whitman) you can fairly easily make sure that you’re consistent with yourself. But when multiple people (who may concurrently change their minds) must work together, consistency often becomes the overriding concern.
This gets technical and difficult. In order to express the propositions that we intend to denote requirements, we must choose some logic. Basic intuitionist logic is enough for e.g., the implication (A -> B -> B) -> B -> [A] -> B to restrict foldr, but it’s possible to imagine much more complex restrictions. In fact, that has led to the explosion of interest in type theory (and formal logic generally) today.
Recursive types allow us to usefully put boundaries on complex data structures. In fact, the combination of sum types and recursive types makes it easy to reason about the intermediate structures produced by parsing context-free grammars, because they map exactly to the structure of non-terminal rule definitions.
Linear types are half of the underpinning of Haskell’s highly successful monads. These linear types allow us to ensure that the values they denote are used once and only once. Especially when we otherwise have a hard time keeping track of the resources we’re using, linear types put a finite extent on the influence of values in our programs. Opened files are closed and network connections go away.
Dependent types can be used to reason about types of runtime values dependent on constant compile-time values. We can use such a type system, for example, to prove that our array accesses are all within bounds, or that we won’t exceed some fixed memory requirement, or even to write a safe printf!
Type reconstruction can be used to infer self-consistency. While this releases programmers from explicitly recording types, it can interact badly with other type rules (like linear and dependent types), and in general the procedure can take an exponential amount of time proportional to the size of your program. Being based on unification, the occurs check question must be answered, which can be a real problem when trying to infer the type of some hairy higher-order functions. However, when computations are simple enough to avoid those problems, type reconstruction is an excellent compromise between explicit annotations (which can be time-consuming and expensive), and potential inconsistencies (which can be arbitrarily expensive in the wrong circumstances).
Going far down this road is not without peril. Following this trail of logic, we might inexplicably end up in an untyped universe. Or in fact we could wrap around the other way and make an inconsistent world incomplete.
Whatever we choose, it’s an issue that I think is well worth considering. It’s important to be able to reason about the environments we share with one another, to avoid being surrounded by core dumps wondering why, or worse:
POZZO: When! When! One day, is that not enough for you, one day he went dumb, one day I went blind, one day we’ll go deaf, one day we were born, one day we shall die, the same day, the same second, is that not enough for you?