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…