Waiting for Gödel

May 9th, 2007

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?

Background:
Types and Programming Languages
Advanced Topics in Types and Programming Languages

4 Responses to “Waiting for Gödel”

  1. andrew cooke Says:

    hi, don’t you have dependent types backwards? did you miss a “not”? afaik, they depend on runtime values (depending on constant compile time values isn’t very hard, is it? an array of fixed compile time length is a tuple, for example).

  2. Locke Says:

    You may want to change the title of this post, I believe you meant it to be “Waiting for Godot”.

  3. Andy Says:

    Locke, I think that was intentional…

    “in general the procedure can take an exponential amount of time proportional to the size of your program.”

    Weren’t the ML folks concerned about this at one point, but no program in the real world has ever caused it to go exponential?

  4. Kalani Thielen Says:

    andrew cooke:

    I don’t think I’ve got it backwards, although there might be some implementations that insert runtime checks if the checker can’t make a decision about equivalence of types. That’s the meaning of the statement “[to] decide typechecking, we therefore need to decide some kind of equivalence up to computation” in this great treatment of the subject. I probably shouldn’t have said “constant values” per se, and just “terms” though. Those values can be arbitrary computations that resolve at compile time (as in the C++ type system).

    I’m not familiar with every implementation of dependent types though, I’ve just used Epigram.

    Andy:

    It’s not generally a problem, you’re right. The people I’ve talked to about it are more concerned about the way type inference interacts with other features of their type systems than of performance problems per se. There probably are some real world programs that have suffered from it though, just going by the law of large numbers. :)