My colleague Jamie already broke the news a while ago, so I guess there's nothing stopping me: my adviser1, Amal, has left Indiana University and joined the faculty at Northeastern. I've sat down to try to write about that a dozen times since Amal told me the news in mid-June, but it appears that my attempts have to do so have instead yielded a 4000-word screed about how my Ph.D. career had been progressing up until about mid-June.
I'd like to share that story with you, but before we start, a warning about me. Some people manage to keep dedicated research blogs that they keep entirely separate from wherever it is, if anywhere, that they write about goings-on in their personal lives. I am not one of those people. I love to write about research, but if I have a research-related epiphany, not only am I going to tell you what it is, I'm going to tell you which metaphorical or actual bathroom stall it happened in. At length. I can do pithy, too, but if "pithy" is what you're after right now, I think you're in the wrong place, friend.
Okay; warning imparted -- off we go, then!
What I usually tell people is that for the last three years, I've been a grad student in the programming languages group at my school. That isn't quite true. In fact, I joined IU without being a member of any research group. In my first year, I had a hooray-you're-a-girl fellowship, so I didn't need to teach or do research in order to have funding; in effect, that meant that I was able to treat the first part of grad school as an extension of undergrad.2 All I had to do was take classes, and that was something I already knew how to do, so I did pretty well at it. I finished my first semester with excellent grades and a feeling of smug superiority to everyone I'd ever heard say that grad school was hard.
Then, Dan asked me to help teach his course during my second semester. My fellowship would have supported me until the end of the year, so I didn't have to teach anything. But I'd loved taking the course in the fall, and I was flattered to be asked to help out, so I went for it. Dan's student at the time, Will, was deeply into dissertation mode, so working for Dan meant a lot of hanging around Will as he worked on miniKanren. That was how I began to dip a toe into research, which is, I'm sure, what Dan had intended to have happen all along. For Dan, teaching and research are inextricably linked. Even just the teaching part by itself was a challenge for me, though, and I was doing it on top of my normal course load, which was harder than the previous semester's, since now all the courses I was taking were covering material I hadn't seen before. I stopped feeling smug pretty quickly, and it wasn't too long before I was really getting killed.3
Halfway through the spring, Dan invited me to spend the summer doing research with him and Will, and I very nearly declined the invitation, because I was exhausted and desperately needed a break. But I wrote to John Stone for advice, and thankfully, he talked me out of saying no. In May, I declared victory over the bloody remains of the semester and stuck around to hang out with Dan and Will over the summer. I think that it was at that point that I stopped treating grad school like Undergrad, Part Deux and started really attempting to be a researcher.
The summer was a mixed bag, though. I got a first publication out of it, and even an attempt at a second, plus quite a lot of free pizza. But I never felt like I knew what the hell I was doing, and now I can put my finger on at least one of the things that was wrong. In a theoretical field like ours, I think that reading is one of the most important parts of doing research, and I wasn't doing nearly enough reading. When I was working on our FLOPS submission, I didn't understand that citing someone else's work should mean not only that you've read and understood the relevant part of that person's work, but also that you've surveyed the rest of the nearby research landscape and come up with a reason why that particular paper, rather than some other one, is the right one to cite for your purposes. You might have to look at several papers for every one you actually end up citing. I was citing all kinds of stuff I hadn't really read. Moreover, because I hadn't read enough papers, I didn't have a sense of what a good research paper was supposed to look like or sound like or be. That all goes a long way toward explaining why the FLOPS submission was rejected. At no point had anyone sat me down and said, "You want to be a researcher? You need to learn to read papers if you want to learn to write them."
Amal joined the faculty at IU that fall, just as my second year was starting, and I took her type theory course and loved it. We began working on research together in the spring, and it started to become clear that working with Amal was a good fit for me. Part of the reason I didn't do very much reading when I was working with Dan is that Dan's modus operandi with students is to give them fiendish puzzles to solve -- koans, you might say -- and then actively discourage them from reading anything that might give away the answer, because that would deprive them of the learning experience that comes from figuring it out for themselves. For a certain kind of learner, I'm sure that that approach leads to enlightenment. For me, as a first-year grad student, it just led to frustration. But Amal was different: she gave me piles of stuff to read! I took two more courses from her during spring and fall 2010, both research seminars, and it was in those courses that I finally started to read a lot of papers. Some were more relevant to me than others, but they all filled the need of getting me to just read a whole lot of PL papers, so that I would know how to read papers and therefore be prepared to absorb information from sources that were relevant.
And "prepared to absorb information" was what I needed to be. The project that Amal had suggested for us to work on was an offshoot of research that she had done with Jacob Matthews in 2008. They had published a paper that dealt with how the parametricity property could be made to hold for a language that was partly statically typed and partly dynamically typed, where the two languages were combined using a Matthews-Findler-style multi-language embedding. Having dynamically typed code in the mix would ordinarily mean giving up on parametricity, but their multi-language system used a technique called dynamic sealing that forces programs to behave parametrically at run-time, or die trying. Dynamic sealing wasn't a new idea, but Jacob and Amal were the first to present a (certain style of) proof that it worked as advertised to preserve parametricity. The only problem was that their work had turned out to have a flaw in it that invalidated the proof.4 But Amal had an idea for fixing the problem, and the plan was that we'd fix it, redo the proof, revise the paper to go along with it, and then publish the updated paper as a journal article together.
The Brian Kernighan quotation goes, "Debugging is twice as hard as writing the code in the first place. Therefore, if you write the code as cleverly as possible, you are, by definition, not smart enough to debug it." This is true of math as well, and the flawed proof that we were to fix employed a technique that I would go so far as to call not only clever, but actually kind of sneaky. (All the best math is sneaky.) When we started on the project in January 2010, Amal thought we'd have it done by May. What actually happened, of course, was that it took until May for me to get enough background knowledge to be able to even start the project. I had only just started studying type theory at all, and I'd only had the briefest of encounters with logical relations as a proof technique, let alone the step-indexed logical relations that this proof used. I couldn't even do an SILR proof, much less debug one. Nor did I understand what a multi-language embedding was, how dynamic sealing worked, or even what parametricity was really all about. So I had a long way to go before I was finally ready to start working on the project in May.
According to the commit logs, I then worked on it from precisely May 1 to May 19, at which point I scuttled off to my summer 2010 internship at GrammaTech and proceeded to not look at the thing for four months. Working at GT was great, but when I came back in the fall after my internship ended and tried to pick up where I'd left off on our project in May, I had a hard time remembering what any of it really meant or where we were headed with it. I flailed a bit, thought a lot, wrote down some notes, and thought I'd gotten a decent handle on things again. But then I went to ICFP in Baltimore at the end of September, and Derek Dreyer asked me a very simple question about the project that I should have been able to answer but couldn't, and I wanted to curl up and die right there under the buffet table.
So I got to work. I worked pretty hard on the project for the rest of that semester -- largely made possible by the fact that I was finally, in my third year, being paid to do research rather than being paid to teach5 -- and I slowly and gradually started to understand what the hell was going on.
In our multi-language system, parametricity on the statically typed side is enforced the way it's usually enforced: to wit, statically, by the type system! But on the dynamically typed side, it's enforced dynamically. A seal is nothing more than a unique value, generated at run-time by
gensym or its equivalent. If you want to hide the number 5, you generate a unique seal, then wrap the 5 in a function that takes a seal as argument and compares whatever seal was passed in to your uniquely generated seal, which the function has stored in its closure. If the function's caller knows the correct seal and passes it in, you'll get the 5 back; otherwise, you'll get an error. It's possible to get information hiding, and therefore parametricity, by creating a seal in a private scope and using it to seal values before handing them out to clients, then unsealing them when they come back. And if dynamically typed code is embedded inside statically typed code, it can use this dynamic sealing mechanism to wrap values that came from the static side and had abstract types that were hidden behind type variables over on that side. Thus parametricity can be enforced even in the part of the system that isn't statically typed. Run-time is a rather strange time to be trying to enforce parametricity, but nevertheless, that's when we were doing it. So if we wanted to show that parametricity was actually being enforced, our proof needed to somehow account for the run-time semantics of our language.
What was needed was a sort of run-time environment that could capture information about the seals that had been generated so far. Then we needed to develop an equivalence relation on terms that was parameterized by just such a run-time environment. Such a relation turns out to be what is known as a Kripke logical relation parameterized by possible worlds.6 As it turns out, step-indexed logical relations are already a special case of Kripke logical relations, because a step index (which is just a natural number, so called because it represents the number of steps remaining for future execution of a program) can be thought of as a very low-information form of "world". Actually, for a lot of situations, that step index turns out to be all you need, so part of the contribution of our paper is to illustrate a situation where a step index alone is not enough. In fact, the reason the original version of the proof was broken was because it tried to use step indices alone. We needed to fix it by using richer worlds that capture information about which seals are generated, when they're generated, and which compile-time entities (in particular, type variables on the statically-typed side of the language) the generated seals correspond to. That's what I finally came to understand after the better part of a year.
The very end of the semester was rough, because I unexpectedly also had my oral qual exam to study for. A few days before the exam, everything that I had been working on and thinking about with regard to both quals and research culminated in a breathless middle-of-the-night email to Dan in which I explained how the step-by-step derivation of the Y combinator in The Little Schemer is precisely analogous to Appel and McAllester's (step-)indexed model of recursive types.7 Dan wrote back, "Thanks so much for sharing this with me. Amal explained it to me, but I did not see the relation with fixpoints. Your description is quite clear because I can relate to types and chapter 9 and much of Davey & Priestly. I think that D&P might hold some insight into how to make step-indexing more beautiful. What a very pretty model." That made me pretty happy, but then, one day later, Stevie sstrickl Strickland and Aaron Turon made me even happier by inviting me to come give a talk at Northeastern's PL seminar in Boston. At that point, I had just committed to starting at Mozilla in March. (Oh, yeah, I was somehow also interviewing at Mozilla while all of this was going on. Oh, and also, getting engaged. Come to think of it, those things may have also had a little to do with the happiness.) So if I were going to do the talk in Boston, it would have to be in February at the latest. In December 2010, February 2011 seemed like a very long time away, so I said, "Sign me up!"
I took the qual exam in mid-December, and I passed, but I didn't make my best showing. I knew that with quals, the only thing that matters is whether you pass. Still, I wanted another chance to really show Amal what I had learned. I knew I'd learned a lot, but we'd been working together for a year and I still had no concrete results to point to other than a shaky paper draft, a half-finished proof, and a predilection for sending spastic emails to Dan in the middle of the night. So I decided that my talk at Northeastern needed to be about the multi-language parametricity project, even though it still wasn't done, and even though Amal was going to be on leave starting in January and wouldn't be around to help much.
I kept working on our proof through January and the early part of February, and I got most of the interesting cases done. It actually turned out to be a good thing that Amal wasn't there to answer my every question, because I learned more from wrestling with the proof on my own and digging up relevant references for myself. Then, in mid-February, I put the proof aside -- still not done, but closer! -- and started working on the talk. I worked really hard on that thing. I probably spent 40 hours working on the slides alone, if you count both times I overhauled them after confronting parts of the project about which my own understanding was fuzzy. One might have thought that working on our proof for so long would have forced me to have confronted those things already, but, embarrassingly, enough of this kind of work is mindless symbol-pushing that it's possible to get quite a long way on a proof without actually understanding some key idea. So it was a good thing that I was choosing to give the talk about this project -- because it made me understand my own project a lot better! I ended up going to Boston at the end of February feeling quite well prepared. The talk went well, and I got a wonderful message from Aaron afterward: "Your talk was one of the most enjoyable and comprehensible in recent memory. I particularly liked your intuitions on the duality between universal and existential types." He was referring to the beginning part of the talk, in which I'd tried to touch on What Parametricity Really Means And Why We Care About It In The First Place. I'd written that part with no guidance from Amal at all, so I was especially glad that Aaron liked it!
Another good thing about working on the talk was that it made me think critically about the way that Amal and I had organized our paper. The paper makes a series
of false starts in which it sneaks something that won't work past
the reader, but then turns around and says "Hah, tricked you! We can't
do it that way. Let's do it this other way." That style of organization didn't seem to work for the talk, so I did it in a different way; it builds up the work in
stages, but doesn't set out to fool the audience. After having written the talk that way, I'm tempted to change the paper to a similar style. I don't know if we actually will, but the point is that before working on the talk, I wouldn't have had enough perspective to be able to make meta-level criticisms of the paper. I feel a lot more comfortable doing so now.
After getting back from Boston, I went on vacation with Alex for a few days; then, I almost immediately moved to California and started working for Mozilla on Rust. Working on Rust didn't quite start out in the way I had expected. The job posting that had originally attracted me to Rust had mentioned its type-and-effect system, which was supposed to track mutability of values in Rust. The Rust team, the posting said, was interested in having a soundness proof of a simple model of Rust as reassurance of the cohesiveness of the type-and-effect system design. I thought that my familiarity with Kripke models would serve me well in working on such a thing, since one of the things Kripke models are good for is reasoning about type safety in the presence of mutable state. (Our parametricity project doesn't deal with mutable state as such, but seal generation is a stateful notion akin to storing a value in a new memory location.) By the time I arrived at Mozilla in March, though, the type-and-effect system was already on its way out of the language.8 So I needed to figure out what I was going to work on instead.
After flipping through a draft of the language manual, I was intrigued by Rust's classless, prototype-based object system with flexible, extensible objects -- pretty unusual for a statically typed language. I asked if the prototype-based stuff was for real, and was told, "Oh, most of that isn't implemented yet; you should implement it!" At that point, Rust had the beginnings of an object system: it was possible to create an object that had methods and fields and call those methods or access those fields from the methods, but objects weren't extensible, methods couldn't be overridden, and there was no form of self-dispatch, so methods couldn't call other methods on the same object except by way of a lengthy workaround. In fact, there wasn't even a "self" (or "this") keyword in the language at that time. So I spent my spring and summer implementing pieces of the Rust object system and learning that those pieces interact with each other in interesting ways. It was a great experience, and I learned a hell of a lot. By the end of the summer, I was also contemplating a thesis proposal idea based on Rust, but now I'm jumping ahead -- more on that will have to wait until the second half of this story.
I was originally only going to be at Mozilla for the summer, but Dave Herman had asked if I could show up any earlier than May, and there was nothing really stopping me, since Amal was going to be on leave anyway. I'm very glad that I arrived at Mozilla in March, because it meant that I had more time to work on my project -- I really needed all five of the months I had. But, moreover, it meant that I got to be there in April when the compiler went self-hosting -- first, the first time that the compiler written in Rust compiled itself, and then, a few days later, the first time that that compiler successfully compiled itself, producing a fixpoint. That was one of the cooler moments in my career so far -- so cool that I got the chills.
And that brings us more or less up to mid-June. I was halfway through my internship when I got the news from Amal, and the timing of it divides grad school in half rather neatly, too. So, sometime soon, I'll write about what's happened since then, and about my plans (and dreams!) for what the second half of grad school will be like.
- I still spell "adviser" in the Grinnell style much of the time. If it's good enough for the Firefox spell-checker, it's good enough for me. (On the other hand, the Firefox spell-checker doesn't approve of "parametricity", so.)
- An external fellowship can be a bad thing for precisely this reason. As Tim points out, "Being employed as a research assistant for a specific professor or research group integrates you socially and binds you to a commitment to deliver a particular kind of results -- a commitment that motivates you to finish your task by any means necessary, including collaborating with others. Having a fellowship empowers you to fuck around for almost three years and never get called on your shit." To be fair, though, the one-year fellowship I had did me a lot of good, because when I arrived at grad school, my formal CS education comprised precisely eight courses, instead of the twelve or sixteen that most people take before entering a CS graduate program. (Or more. At one point, I asked Alex oniugnip to count how many CS courses he took at Georgia Tech -- he took twenty-two as an undergrad alone.) So the fellowship turned out to be a good thing, because at the beginning I really needed some time to concentrate on taking classes. But I think I'd be worse off had it gone on any longer.
- It also didn't help that I kept going off to attend workshops that were only vaguely academic. I remember walking across campus at some point in April of 2009, trying to find a place where I could sit and work on my compiler. I couldn't decide where to go, so I thought to myself, "Where have I consistently been able to get a lot of work done on this project?" Then I realized that the answer was "SFO". When you live in Indiana, that's a strange realization to have.
- Neis, Dreyer, and Rossberg writing in JFP this year about the Matthews and Ahmed 2008 paper: "A key technical difference is that their formulation of the logical relations does not use possible worlds to capture the type store (the latter is left implicit in their operational semantics). Unfortunately, this resulted in a significant ﬂaw in their paper. They have since reportedly ﬁxed the problem -- independently of our work -- using a technique similar to ours, but they have yet to write up the details." We're working on it!
- Or to be female.
- Actually, this is redundant, since as far as I can tell, authors in my field use "Kripke logical relation" interchangeably with "logical relation that is parameterized by possible worlds". (After squinting at the relevant Wikipedia talk pages, I see that not everyone is happy about the terms being used interchangeably, but I'm a computer scientist, not a logician, so for me, that's splitting hairs.) In her dissertation, Amal points out that Kripke models are named in honor of logician and philosopher Saul Kripke (you know; the Naming and Necessity guy), citing the 1963 paper in which he developed a model theory for propositional modal logic. But for the most part, PL authors don't seem to cite Kripke when they use Kripke LRs. From the point of view of a PL researcher, his work was general enough and long enough ago that I think citing him would be kind of like citing Alonzo Church every time you write a lambda. (Although that would be kind of awesome.) In fact, there are two POPL 2011 papers that actually mention Kripke LRs in the title, but neither cites Kripke at all.
- And, more generally, that the notion of stratification in domain theory is analogous to the notion of stratification in Kripke models. Up until that point, I'd thought of domain theory, if I thought of it at all, as some difficult and mysterious thing that we didn't have to use because we used Kripke models instead. Now I recognize domain theory and Kripke models as sharing an essential ingredient.
- It turns out, though, that some of the ideas that the type-and-effect system was about are working their way back into the language by way of the kind system.