Conor McBride leads the Mathematically Structured Programming group at the University of Strathclyde, in Glasgow, Scotland. He has been building programming languages for thirty years and is still unhappy with them. His postdoctoral work on the dependently typed functional language Epigram helped to provoke the design of Agda and of Idris. His Haskell preprocessor, the Strathclyde Haskell Enhancement, provoked the DataKinds extension in GHC. He is always looking to bring the mathematical structure of types and programs off the blackboard and onto the motherboard. He is also a working programmer.
YOW! Lambda Jam 2016 Brisbane
What are Types for, or are they only Against?
KEYNOTE – WATCH VIDEO
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.