Peter Seibel - Coders at Work - Reflections on the craft of programming

Seibel:So that points out that there are programs that are correct, because you’re assuming a legitimate source-to-source transformation, which, if you had written it by hand, the compiler would have said, “I’m sorry; I can’t type this.”

Peyton Jones:Right. That’s the nature of static type systems—and why dynamic languages are still interesting and important. There are programs you can write which can’t be typed by a particular type system but which nevertheless don’t “go wrong” at runtime, which is the gold standard—don’t segfault, don’t add integers to characters. They’re just fine.

Seibel:So when advocates of dynamic and static typing bicker the dynamic folks say, “Well, there are lots of those programs—static typing gets in the way of writing the program I want to write.” And then the fans of static typing say, “No, they exist but in reality it’s not a problem.” What’s your take on that?

Peyton Jones:It’s partly to do with simple familiarity. It’s very like me saying I’ve not got a visceral feel for writing C++ programs. Or, you don’t miss lazy evaluation because you’ve never had it whereas I’d miss it because I’m going to use it a lot. Maybe dynamic typing is a bit like that. My feeling—for what it’s worth, given that I’m biased culturally—is that large chunks of programs can be perfectly well statically typed, particularly in these very rich type systems. And where it’s possible, it’s very valuable for reasons that have been extensively rehearsed.

But one that is less often rehearsed is maintenance. When you have a blob of code that you wrote three years ago and you want to make a systemic change to it—not just a little tweak to one procedure, but something that is going to have pervasive effects—I find type systems are incredibly helpful.

This happens in our own compiler. I can make a change to GHC, to data representations that pervade the compiler, and can be confident that I’ve found all the places where they’re used. And I’d be very anxious about that in a more dynamic language. I’d be anxious that I’d missed one and shipped a compiler where somebody feeds in some data that I never had and it just fell over something that I hadn’t consistently changed.

I suppose static types, for me, also perform part of my explanation of what the program does . It’s a little language in which I can say something, but not too much, about what this program does. People often ask, “What’s the equivalent of UML diagrams for a functional language?” And I think the best answer I’ve ever been able to come up with is, it’s the type system. When an object-oriented programmer might draw some pictures, I’m sitting there writing type signatures. They’re not diagrammatic, to be sure, but because they are a formal language, they form a permanent part of the program text and are statically checked against the code that I write. So they have all sorts of good properties, too. It’s almost an architectural description of part of what your program does.

Seibel:So do you ever write a program that you know is correct but somehow falls outside the bounds of the type checker?

Peyton Jones:This comes up when you’re doing generic programming, where you want to write functions that will take data of any type and just walk over it and serialize it, say. So that’s a time when types can be a bit awkward and an untyped language is particularly straightforward. It couldn’t be easier to write a serializer in an untyped language.

Now there’s a small cottage industry of people describing clever typed ways of writing generic programs. I think such things are fascinating. But it’s somehow just isn’t as simple as writing it in a dynamically typed language. I’m trying to persuade John Hughes to write a paper for the Journal of Functional Programming on why static typing is bad. Because I think it would be very interesting to have a paper from John, who’s a mainstream, strongly typed, very sophisticated functional programmer, who is now doing a lot of work in untyped Erlang, saying why static types are bad. I think he would write a very reflective and interesting paper. I don’t know quite where we’ll end up.

I think I would still say, “Where static typing fits, do it every time because it has just fantastic maintenance benefits.” It helps you think about your program; it helps you write it, all that kind of stuff. But the fact that we keep generating more and more sophisticated type systems is an indication that we’re trying to keep pushing the boundary out to say more in the world—to cover more programs. So the story hasn’t finished yet.

The dependently typed programming people would say, “Ultimately the type system should be able to express absolutely anything.” But types are funny things—types are like a very compact specification language. They say something about the function but not so much that you can’t fit it in your head at one time. So an important thing about a type is it’s kind of crisp. If it goes on for two pages, then it stops conveying all the information it should.

I think the direction I’d like to see things go is to have still crisp and compact types which are a little bit weak, precisely so that they can be crisp, along with invariants, perhaps stated in a rather richer language than the inferable type system, but which are still amenable to static checking. Something I’m working on in another project is to try to do static verification for pre- and post-conditions and data-type invariants.

Seibel:Similar to Design by Contract in Eiffel?

Peyton Jones:That’s right. You’d like to be able to write a contract for a function like, “You give me arguments that are bigger than zero and I’ll give you a result that is smaller than zero.”

Seibel:How do you go about designing software?

Peyton Jones:I suppose I would say that usually the dominant problem when I’m thinking about writing a program—thinking about writing some new piece of GHC—is not how to get the idea into code. But it’s rather, what is the idea?

To take an example, at the moment we’re in mid-flight for moving GHC’s back end, the code generation part, to refactor it in a new way. At the moment there’s a step in the compiler that takes essentially a functional language and translates it into C--, which is an imperative language. And that’s a pretty big step. It’s called C-- because it’s like a subset of C. But it’s really meant to be a portable assembly language. And it’s not printed out in ASCII—it’s just an internal data type. So this step in the compiler is a function from a data structure representing a functional program to a data structure representing an imperative program. How do you make that step?

Well, I have a pretty complicated bit of code that does that at the moment. But a couple of days ago I realized that it could be separated into two parts: first transform it into a dialect of C--, which allows procedure calls—inside a procedure, you can call a procedure. Then translate that into a sub-language that has no calls—only has tail calls.

Then the name of the game is figuring out, just what is the data type? This C-- stuff, what is it? It’s a data structure representing an imperative program. And as you make the second step, you walk over the program, looking at each bit, one at a time. So your focus of attention moves down the control flow, or perhaps back up through the control flow. A good data structure for representing that is called a “zipper”—which is a very useful purely functional data structure for moving the focus around a purely functional data structure.