What are Types for, or are they only Against?
Doctor Who: I think my idea’s better. Lester: What is your idea? Doctor Who: I don’t know yet. That’s the trouble with ideas: they only come a bit at a time.
(from “Revenge of the Cybermen” episode 3, by Gerry Davis)
Much of the perennial wrangling about types and type inference is predicated on the traditional man-proposes-God-disposes model of editor-compiler interaction.There often also lurks an assumption that the term language component of program texts should entirely determine what it is that programs do.Advocates of types often emphasize the bad behaviours types prevent, not any kind of goodness types sustain.This century, neither of these assumptions is necessary.I shall argue that, moreover, neither is helpful, and hence that we should stop rehashing last century’s battles on the internet.
The utopian position is to consider types as design statements, proposed in advance.The program text can be constructed by a joint effort of humans and machines.It should document the interesting parts of the explanation of what the program does, minimally the choices made by the humans which are not forced by the types.Types can describe a lot more that the machine representation of data: they can also characterize computational structure in ways which trigger code generation. Moreover, if we program in incremental interaction with a typechecker, we can work by stepwise refinement from specification to implementation.We are thus incentivized to write precise types. Of course, this position also makes the false assumption that we know what we are doing before we are doing it.
Looking to the future, I shall consider what programming language designers and programming tool developers might do to support ideas, even though the trouble is that they only come a bit at a time.