What are Types for, or are they only Against?
Please log in to watch this conference skillscast.
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.
YOU MAY ALSO LIKE:
What are Types for, or are they only Against?
Conor McBride
Dr Conor McBride runs the Mathematically Structured Programming group at the University of Strathclyde. He specialises in dependently typed programming. Over a decade ago. he was co-designer and implementer of Epigram. These days, while working on foundational innovations beyond advanced languages like Agda and Idris, he also engages keenly with the languages funcitonal programmers use for real work today. He is one of the people helping to drive the evolution of Haskell's type system towards ever greater expressivity.