BREAKING: What the second half of grad school will be like

Back in September, I wrote about what the first half of grad school was like for me. That post covers a period of about three years, from the middle of 2008 to the middle of 2011. I've been wanting very much to write the companion piece covering the second half of grad school, but so far, I've been hampered by the fact that most of the second half of grad school has not actually transpired yet.

Still, I'm willing to give it a shot!¹

To recap from last time: while I was at Mozilla working on Rust last summer, my advisor invited me to come with her to Northeastern University for the rest of my Ph.D., which meant that I had to choose between IU and NU. It was an extraordinarily difficult decision to make. NU has a world-class group of PL researchers; living in Boston probably would have been cool; and, of course, I'd have gotten to keep working with Amal in person. But my husband, Alex, is also in the middle of his Ph.D., and while it hasn't been nonstop rainbows and sunshine for him here at IU, starting over at yet another school (assuming he could find a graduate program in Boston that was a good fit for him), and then probably having to take yet more courses and jump through more qualifying exam hoops, would be far worse. Living apart isn't a viable option for us, either -- we did that for a year and a half, and we're not interested in trying to do it again. (Empirically, if we're apart for more than a week these days, I go nocturnal and spend all my time either reading genre fiction or watching the same Lady Gaga video over and over. Bad scene.)

So, when I got back to school last August, I started working with a new advisor, Ryan Newton, who had just joined the faculty at IU. I'm now being advised by both Amal and Ryan, but Ryan is who I see day to day. I've spent a lot of time in the last several months telling Ryan about my work with Amal, and now that Ryan and I have a project going as well, I've started to do some of the reverse. Happily, I learn a lot in the process of doing so!

In order to get a better sense of the kind of research Ryan does, I took his course on embedded DSLs for parallelism in the fall. This was a new area for me to be reading in, and one of the papers that particularly grabbed me was about the Concurrent Collections system that Ryan had worked on while he was at Intel (abbreviated "CnC", as per some Intel marketing team). The paper had a proof of determinism for a parallel language called Featherweight CnC that's a lightweight model of full CnC. I noticed that the determinism proof hinges on a monotonicity lemma that says that if one state s in the semantics steps to another state s', then either s' is an error, or the store in s' is a valid extension of the store that s had. The monotonicity lemma, in turn, hinges on a single-assignment property, which states that we can only write to previously unused memory locations. It was the sort of thing that smelled like it might fit into a possible-worlds semantic model like the ones that I have some familiarity with from working with Amal. I was also curious about the analogy between the single-assignment property and the "weak updates only" requirement that some systems have, which requires that updates to a store can only change the value, not the type, of the contents of a cell -- and whether any of the tricks that allow loosening of the weak-updates-only requirement had analogues that would allow loosening of the single-assignment restriction.

When I went to talk to Ryan about that, it turned out that he had also been thinking about loosening the single-assignment restriction on single-celled I-structures, sometimes known as IVars, which are the communication mechanism that the Haskell monad-par package uses. If it's okay to write to a cell once, it seems like it should be fine to write the same value multiple times. But at that point, it would be interesting to try to loosen the notion of "same" and replace it with a less restrictive equivalence relation. "Values that unify with each other" is one possibility that Ryan brought up; for me, good ol' "values that are indistinguishable for a given number of steps" comes to mind. Also, what would happen if we parameterized a language by an equivalence relation for sameishness, lambda-eek-style? What properties would have to hold of that equivalence relation to make the language