Seibel Peter. Coders at Work
Подождите немного. Документ загружается.
Simon Peyton Jones
265
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.
Norman Ramsey at Harvard found a way to use this for walking around data
structures that represent imperative control flow graphs. So he and I and
John Dias then spent a while reengineering GHC’s back end to adopt
essentially this factored technology. And in doing so making it much more
general so we can now use this same back end as a back end for other
languages.
A lot of our discussion was essentially at the type level. Norman would say,
“Here’s the API,”—by giving a type signature—and I would say, “That looks
way complicated, why is it like that?” And he’d explain why and I’d say,
“Couldn’t it be simpler this way.” So we spent a lot of time to’ing and
fro’ing at the level of describing types.
But a lot of the time it wasn’t really about programming as such—it was
about, what is the idea? What are we trying to do with this dataflow
analysis, anyway? You try to say in a clear way what this step of the program
is meant to do. So we spent quite a lot of time just being clear on what the
inputs and the outputs are and working on the data types of the inputs and
the outputs. Just getting the data types right, already you’ve said quite a lot
about what your program does. A surprisingly large amount, in fact.
Seibel: How does thinking about the types relate to actually sitting down
and coding? Once you sketch out the types can you sit down and write the
code? Or does the act of writing the code feed back into your
understanding of the types?
Peyton Jones: Oh, more the latter, yes. I’ll start writing type signatures
into a file right away. Actually I’ll probably start writing some code that
manipulates values of those types. Then I’ll go back and change the data
types. It’s not a two-stage process where we say, “Now I’ve done the types,
I can write the code.”
Download at Boykma.Com
Simon Peyton Jones
266
If anything I’m a bit ill-disciplined about this. This comes from not working
as part of a large team. You can do things when you’re working on code
that one person can still get their head around that you probably couldn’t in
a much bigger team.
Seibel: You mentioned that in this latest code upheaval in GHC, things got
much more general. GHC is a big program that’s evolved over time so
you’ve had the chance to benefit from generality and the chance to pay the
cost of over-generality. Have you learned anything about how to strike the
balance between over- and under- generalization?
Peyton Jones: I think my default is not to write something very general to
begin with. So I try to make my programs as beautiful as I can but not
necessarily as general as I can. There’s a difference. I try to write code that
will do the task at hand in a way that’s as clear and perspicuous as I can
make it. Only when I’ve found myself writing essentially the same code
more than once, then I’ll think, “Oh, let’s just do it once, passing some extra
arguments to parameterize it over the bits that are different between the
two.”
Seibel: What is your actual programming environment? What tools do you
use?
Peyton Jones: Oh, terribly primitive. I just sit there with Emacs and
compile with GHC. That’s just about it. There are profiling tools that come
with our compiler and people often use those for profiling Haskell
programs. And we do that for profiling the compiler itself. GHC dumps a lot
of intermediate output so I can see what’s going on.
Debugging, for me, is often, the compiler isn’t generating good code so I’m
eyeballing the state of its entrails. Or, take this little source program;
compile it this far; look at that. That’s debugging for me. It’s seldom single-
stepping through the program—it’s more looking at values of different parts
in compilation.
I don’t even have any very sophisticated Emacs jiggery-pokery. Which some
people do. There’s also a whole world of people out there who are used to
Visual Studio and Eclipse kind of IDEs. I think a cultural barrier to adoption
of functional programming languages is partly that we haven’t got the IDE
Download at Boykma.Com
Simon Peyton Jones
267
story sorted out. There’s a bit of a chicken-and-egg problem here. At the
moment the chicken is getting busier—there’s more interest in functional
programming generally. I’m hoping that will provoke work on the egg. It’s a
lot of engineering to build an IDE for Haskell. Even with Visual Studio as a
shell or Eclipse as a shell, there’s quite a lot of work in making a plugin that’s
really smooth and does everything right.
Seibel: GHC has a read-eval-print loop, GHCI. Do you tend program
Haskell interactively?
Peyton Jones: Actually, I tend to mostly edit and compile. But other
people just live their whole lives in GHCI.
Seibel: When it comes to testing, I suppose one of the nice things about
functional languages is when you want to test some little function in the
bowels of your program, you just have to figure out what form is its input
going to be.
Peyton Jones: Well, for me, if the input data is simple enough that you
could do that, it’s probably not going to be the problem with my program.
The problem with my program is going to be some fairly humongous input
program that GHC is trying to compile and getting the wrong answer for it.
Testing is, I think, frightfully important for writing down properties and
QuickCheck properties are really useful—QuickCheck is a Haskell library
for generating random tests for a function based on its type. But I was trying
to think why I don’t use QuickCheck—which is a very nice tool—more. I
think it’s because the situations that cause me trouble are ones that I would
find it difficult to generate test data for. In any case, there are loads of
people out there generating programs that make GHC barf in one way or
another. That’s what GHC’s bug tracker is about.
So typically I’m starting with something that’s not right, already. Maybe the
compiler could just fall over altogether or reject a program when it
shouldn’t. Or it could just generate suboptimal code. If it’s just generating
bad code, I’ll look at the code at various stages in the compilation pipeline
and say, “It looks good then; it looks good then. Bah, it’s gone bad here;
what’s gone wrong?”
Download at Boykma.Com
Simon Peyton Jones
268
Seibel: So how do you actually look at it?
Peyton Jones: GHC has flags that let you say, in rather a batch-dumpy kind
of way, “Just print out various things.”
Seibel: Built-in print statement debugging?
Peyton Jones: Yes. And it’s aided by the fact that the structure is like most
compilers: it has this top-level structure of a pipeline of things that happen.
If something’s gone wrong in the middle of one of these passes, then that
could be a bit trickier. But I tend to use rather unsophisticated debugging
techniques. Just show me the program before and after this pass. Aaah, I see
what’s going wrong. Or sometimes I don’t see what’s going wrong so then I
might scatter a few unsafe
printfs around to show me what’s actually going
on.
There are various debugging environments for Haskell—a summer student,
Pepe Iborra, did a nice one earlier this year which now comes with GHC,
which is an interactive debugger of some kind. Which I’ve not used very
much yet. Partly because we haven’t had one for so long, because it’s less
obvious how do you single-step a functional program.
It’s been a kind of interesting research question of how you go about
debugging functional programs for some time. It’s a bit embarrassing that we
can’t tick that box in a straightforward way, but that makes it an interesting
research problem.
That was the long way around of saying that I tend to use terribly crude
debugging techniques with unsafe
printfs. And I’m not very proud of that.
But for a long time we didn’t have anything else. At least as far as GHC is
concerned, I’ve evolved mechanisms that mean that’s the shortest path to
completion for me.
Seibel: That seems to be a common story. It sort of makes you wonder
about the utility of writing better debuggers if so many people get by with
print statement debugging.
Peyton Jones: There’s a cultural thing though. On the .NET platform with
debuggers that people have put tens or hundreds of man-years into
Download at Boykma.Com
Simon Peyton Jones
269
engineering, I think it’s a qualitatively different experience. I think debuggers
do require perhaps more engineering cycles to get to work well. But if you
put them in, you do get something that is really quite remarkably more
helpful.
Maybe the people that you’ve been mainly talking to are more in the
academic software mold. And also perhaps have grown up with
sophisticated debugging environments less. I wouldn’t like to draw any
general lessons. I certainly wouldn’t wish to denigrate or downplay the
importance of good debugging environments. Particularly in these rather
complicated ecosystems where there are many, many, many layers of
software. GHC is a very simple system compared to a full-on .NET
environment with layers of DOMs and UMLs and I don’t know what kind of
goop. The real world gets so goopy that more mechanical support may well
be really important.
Seibel: Another approach to getting correct software is to use formal
proofs. What do you think about the prospect of that being useful?
Peyton Jones: Suppose you declare that your goal is for everything to have
a machine-checked proof of correctness. It’s not even obvious what that
would mean. Mechanically proved against what? Against some specification.
Well how do you write the specification? This is now meant to be a
specification of everything the program does. Otherwise you wouldn’t have
proved that it does everything that it should do. So you must have a formal
specification for everything it should do. Well now—how are you going to
write that specification? You’ll probably write it in a functional language. In
which case, maybe that’s your program.
I’m being a bit fast and loose here because you can say some things in
specification languages that you can’t say in programs like, “The result of the
function is that y such that y squared equals x.” That’s a good specification
for a square-root function but it’s not very executable. Nevertheless, I think
to try to specify all that a program should do, you get specifications that are
themselves so complicated that you’re no longer confident that they say
what you intended.
I think much more productive for real life is to write down some properties
that you’d like the program to have. You’d like to say, “This valve should
Download at Boykma.Com
Simon Peyton Jones
270
never be shut at the same time as that valve. This tree should always be
balanced. This function should always return a result that’s bigger than
zero.” These are all little partial specifications. They’re not complete
specifications. They’re just things that you would like to be true.
How do you write those down? Well, functional languages are rather good
at that. In fact this is exactly what happens when you write a QuickCheck
specification; you write down properties as Haskell functions. Say we want
to check that
reverse is its own inverse—well, you might write
checkreverse with type list of A to bool. So checkreverse of xs is reverse
of reverse xs equals xs. So this is a function that should always return true.
That’s what a property function is. But it’s just written in the same
language—so that’s nice.
Now you might hope to do some static checking on this. It might be hard or
easy. But even having the property written down in a formal way is a real
help. You can test it by generating test data, which is, indeed, just what
QuickCheck does.
So rather than trying to write down specifications for all that a program
does I think it’s much more productive to write down partial specifications.
Perhaps multiple partial specifications. And then check them either by
testing or by dynamic checks or by static checks. You never prove that your
program is right. You just increase your confidence that it’s right. And I
think that’s all that anybody ever does.
Seibel: So you define however many properties, covering the things you
care about. And then you can choose to confirm that those properties
actually hold either statically or dynamically, depending on what’s actually
feasible. Because we may not know how to statically check them all?
Peyton Jones: Right. But in a functional setting, you have a better chance.
But we’ve still been dragging our feet a bit about demonstrating that.
Nevertheless—step one is to write down these properties in the first place.
But I think the big thing is to get away from this monolithic, all-or-nothing
story about specification and to say that you can do useful static and
dynamic tests on partial specifications. These will increase your confidence
in the correctness of your program and that is all you can possibly hope for.
Download at Boykma.Com
Simon Peyton Jones
271
Even the allegedly complete specifications miss out—you know, it has to
work in .1 of a second. Or must fit in 10KB of memory. Resource things are
often not covered. Or timing things. There’s endless little stuff that means
the program might actually not function as desired even though it meets its
formal specification. So I think we’re kidding ourselves to say we’ve actually
proved the whole thing is completely right. Best thing to do is to
acknowledge that and say we’re improving our confidence—that’s what
we’re doing. And that can start quite modestly—you might have improved
your confidence by 75 percent with only 5 percent of the effort. That’d be
good.
Seibel: Let’s talk about concurrency a little bit. Guy Steele asked me to ask
you: “Is STM going to save the world?”
Peyton Jones: Oh, no. STM is not going to save the world on its own.
Concurrency, and parallel programming generally, is a many-faceted beast
and I don’t think it will be slain by a single bullet. I’m a diversifist when it
comes to concurrency.
It’s tempting to say, “Use one programming paradigm for writing concurrent
programs and implement it really well and that’s it;” people should just learn
how to write concurrent programs using that paradigm. But I just don’t
believe it. I think for some styles of programming you might want to use
message passing. For others you might want to use STM. For others data
parallelism is much better. The programmer is going to need to grapple with
more than one way to do it.
But if you ask me, is STM better than locks and condition variables? Now
you’re comparing like with like. Yes. I think it completely dominates locks
and condition variables. So just forget locks and condition variables. For
multiple program counters, multiple threads, diddling on shared memory on
a shared-memory multicore: STM. But is that the only way to write
concurrent programs? Absolutely not.
Seibel: A criticism I’ve heard of STM was that when it really gets down to
it, optimistic concurrency won’t allow as much concurrency as you hope. I
think the claim was you can fairly easily get in these situations where you’re
really not making progress.
Download at Boykma.Com
Simon Peyton Jones
272
Peyton Jones: You do have to worry about starvation. My favorite
example here is of one big transaction that keeps failing to commit because
a little transaction gets in there and commits first. So an example would be a
librarian who’s reorganizing their library. They start optimistically
reorganizing their library. And they’ve got two-thirds of the way through
and an undergraduate comes along and borrows a book. Well, he commits
his transaction successfully because the library reorganization hasn’t
committed. The librarian gets to the end and discovers, ah, I saw an
inconsistent view of memory because the library changed while I was
reorganizing it so I just have to go back and start again.
Seibel: In a locks-and-condition-variables program it would probably go the
other way—the librarian would lock the library and nobody could check out
books until it’s completely reorganized. So you would probably look at this
problem and immediately say, “We can’t lock the library until we’re done,”
disallowing checkouts so we have to come up with some hairier locking
scheme.
Peyton Jones: Right. Make a little sub-library or something—put the
commonly borrowed books out there so undergraduates can borrow them
while you lock the main library and reorganize it or something. So now
you’ve got to think of an application-specific strategy and now you’ve got to
express it in some way. Well, the same problem arises in both cases—you
need an application-specific strategy so you can reorganize the library
despite not wanting to block out all sorts of borrowing. Once you’ve done
the hard thinking about how you wish to do it, now you’ve got to express
that. What is the medium in which to express it? STM is a clear win. It’s just
much better than locks and condition variables for expressing concurrent
programs.
Seibel: What if I don’t even want to allow for the possibility that someone
comes in and looks for the 21st most-requested book and gets blocked? In
the physical world you can imagine that when someone checks out a book
we swap in a proxy for the book that the librarian then reorganizes and
whenever a book comes back we put it back wherever the proxy is now.
But you are modifying the library which seems, in an STM world, like it
would cause the librarian to have to retry his whole transaction.
Download at Boykma.Com
Simon Peyton Jones
273
Peyton Jones: But there’s something that stayed the same—the key on the
book is guaranteed not to change somehow, right? So there’s a number of
ways you could do this. One is you could say, “What you do when you
replace it with a proxy is you don’t modify the library at all”—that’s
unchanged. What you do is you modify the book itself. And you don’t
modify its key field—you only modify its value field, where it’s currently
living. Now the index can be reorganized while the book is somewhere else.
That’s cool—and you can express that perfectly naturally.
With STM, at the end the librarian looks through all the memory locations
that he has read and sees if they contain now the same values that they did
when he read them. So the locations that he has read will include the key
field of the book because that determined where he put it. But he hasn’t
read the contents of the book. So he’ll say, “Ah, this book—does this key
field still contain 73; oh, yes it does.”
But I don’t want to minimize the problem of starvation because it’s a bit
insidious. You need good profiling tools that point you at transactions that
are failing to commit because they keep getting bumped so that, rather than
the program just silently not doing very much, you get some feedback about
it. The same is true of a lock-based program. I hate it when those
hourglasses appear.
Seibel: I guess in locked-based programs we’ve just learned to try hold
locks for as short a duration as possible since that will give us the least
contention.
Peyton Jones: Right. But, of course, then it’s harder to program. Finer-
grained locking is tricky to get right. I think this is one of the huge wins of
STM, is it gives you the fine granularity of very fine-grained locking along
with very simple reasoning principles.
Here’s a reasoning principle that STM gives you that locks absolutely do not.
I’ll establish my top-level invariants—I’ve got a bunch of bank accounts, the
total sum of money in all the bank accounts added together is N. Money
moves between bank accounts—that’s all. So there’s my invariant. Any
transaction assumes that invariant at the beginning and restores it at the
end. How do you reason that it does? We look at any one transaction that
says, “Take three out of that one and put three into that one.” Good,
Download at Boykma.Com
Simon Peyton Jones
274
invariant maintained. How is my reasoning in that done? Purely sequential
reasoning. Once I’ve described some top-level invariants, I can reason
completely sequentially about each transaction separately.
Seibel: Because you have transaction isolation.
Peyton Jones: Because they are put in isolation. So that’s really rather a
powerful reasoning principle. Because it says you can use your sequential
reasoning about imperative code despite the fact that the program’s
concurrent. You’ve got to establish what those top-level invariants are, but
that’s good for your soul, too. Because then you know what things you are
trying to maintain. If you get an exception thrown in the middle of a
transaction, that’s cool, too—that can’t destroy the invariants because the
transaction is abandoned without effect. I think this is fabulous. Then
reasoning about performance issues is a different level—you’ve guaranteed a
certain sort of correctness; now you want to make sure you haven’t got any
performance holes. Those are harder to get at—at the moment I don’t
know anything better than profiling and directed feedback tools for doing
that.
Seibel: It strikes me that while optimistic concurrency has been used from
time to time in persistent databases, it’s never really gotten a foothold there
compared to lock-based concurrency.
Peyton Jones: Of course STM can be implemented in all sorts of ways—
optimistic concurrency is only one of them. You can lock as you go, which is
more like a pessimistic concurrency model.
Seibel: But there’s also a reason that lock managers are the hairiest part of
databases.
Peyton Jones: Right. So the thing about STM is you want to make sure
that one person, or one team, gets to implement STM and everybody else
gets to use it. You can pay them a lot of money and shut them in a small
dark room for a year to try to make sure they do a really good job.
But then that work is usable by everybody through a very simple interface.
That’s what I think is nice about it. What I want to avoid is having that level
of expertise in everybody’s head. The example that I used at a talk I gave
Download at Boykma.Com