People of Programming Languages
An interview project in conjunction with POPL 2018
Interview with Stephanie Weirich
Stephanie Weirich is a Professor at the University of Pennsylvania. She won the 2016 SIGPLAN Robin Milner Young Researcher Award and her 2006 paper with Simon Peyton Jones, Dimitrios Vytiniotis, and Geoffrey Washburn, “Simple unification-based type inference for GADTs,” was recognized by the 2016 Most Influential ICFP Paper award. In this interview we talk about her approach to language design and her experience working with adding new features to Haskell, a language that started in research but now has many industry users.
JY: Tell us about yourself. How did you come to work on what you do now? What are you most excited about these days?
SW: My first introduction to programming languages was when I was an undergraduate at Rice University. I took classes in programming languages there and I did an undergraduate research project with Matthias Felleisen’s group and that captured my interest in the foundational nature of programming languages. From there, I went onto Cornell University for my graduate work and worked with Greg Morrisett on type systems and functional programming. When I finished at Cornell, I immediately came to Penn and started as an Assistant Professor, and I have remained fascinated with type systems, especially in functional programming languages.
JY: Could you talk about your motivation for working on dependent types?
SW: Some of my motivation was I that appreciated the structure that static type systems bring to programming languages. However, there were certain programs that were difficult to type-check statically. I did all my undergraduate work in Scheme, a dynamically typed language, and I didn't want to give up those programs. I wanted to bring that capability to a setting where we had the structure of types as well.
JY: I was curious about how you started working with Haskell.
SW: It’s a funny story. I was working on project with Karl Crary and Mike Hicks about a type system for a low level language with dynamic updating. You could bring in new code dynamically and part of that would be you have to know what type of code it was. While I was thinking about how I could do a run time type check in this setting, I had this great encoding of run time type checks. I didn't know this at the time, but it was really an encoding of Leibniz equality. However, for the encoding, I needed higher order polymorphism. That was something that ML didn't have, or it only had through the module language. But I wanted to capture this idea I had in a functional language and show it to other people. I couldn't really do it very well in ML, so I tried it out in Haskell, and that my first Haskell program that I wrote. That turned into a paper that I had at ICFP 2000. But I wasn't intending to make work on the Haskell type system a focus of my research after that—that was just this fun project I was working on.
What happened later was that after I had moved to Penn and I was looking around for new projects to work on, Simon Peyton Jones contacted me and said, "Hey, I want to have something that kind of looks like those run-time type representations that you had so long ago, but more general." Simon is such a fantastic collaborator. I jumped at the chance to work with him. That eventually turned into the paper on adding in GADTs to GHC. Once I started working with Simon, I was hooked on both collaborating with him and also working on the Haskell type system in general.
JY: You've been working on Haskell since the early days, right?
SW: Haskell '98 happened before I ever touched the language, but ever since 2000 I've been playing with the language and the types.
JY: What was Haskell like when you started? It's hard to imagine Haskell without GADT's or a lot of the other stuff that you worked on.
SW: Yeah, changes happen incrementally, so it's really hard to remember, but it's not all that different from Haskell today. What's different is now is there's a lot more people using Haskell than there used to be. There are many people who use Haskell without extensions and they program very close to what Haskell looked like when I just started. Of course now we also have a lot of people who really go out and test drive these extensions and te see what they can do. That's something that's really fantastic for me as a language researcher because I have some ideas of what type systems extensions are for, and there's usually a program when I think about an extension. But, I can't think of all of those programs. It's still fabulous to read about new libraries coming from industry that use these extensions in ways I never could have thought of.
JY: What's been your interaction with industry users of Haskell? Do you talk to them? Do they talk to you? Do you get them to try out your ideas before you publish them?
SW: Not so directly. I have been to a couple of developer conferences specifically so that I can talk to people and find out what they're using. I also spend time with Hackage, taking a look at the code that's out there to see the impact that a change would have on average Haskell programmers. For example, when we were working on explicit type applications, I spent a long time looking to see how people used proxies, which is kind of a work-around for type applications. This helped me understand what were some of the opportunities that people would find with the extension. Of course, this isn’t everything because once you make something easier to use, more people use it. But, it was a way for me to figure out whether the extension was worth doing.
JY: How do you choose problems? Is it more than you have a vision for what programmers would use if they had it, or do you start more with what you observe programmers struggling with right now?
SW: It's more the former. With dependent types, I spent a lot of time programming with Coq and Agda so that I could see better what was lacking from Haskell. I also spend a lot of time observing—through conference calls talking to Simon, talking to my students, talking to other collaborators, and other people who work on Haskell. I feel like I spend a lot of time just trying to figure out what the real problem is, though. It is not just what or how we could add something new, it also involves studying interaction with what's already there. For questions like that I work more theoretically. I make a model of Haskell's type system and I say, "What if I added this to it? What does that change about the theory?"
JY: I wanted to get back to something you said that struck me, which was that you spend a lot of time programming in languages like Coq and Agda. I was wondering what your active programming practice has been like.
SW: I program because it's fun and because I learn a lot from it. When I was really trying to figure out what's going on in dependent types I didn't really think I could get a fair understanding without working through some of the Agda tutorials and seeing for myself what it was like and what it could do. A lot of the programming I do is justified by the class I'm teaching, such as my Haskell course. I get to build up assignments for that course, which is fantastic. So that gives me an opportunity to not just look around and see what other people have done in their functional programming courses, but think also creatively about what I could do with Haskell. Furthermore, making a good homework problem requires you to analyze a program in a way that often tells you about the language itself.
JY: What do you like most about the POPL community?
SW: I've been to POPL thirteen times. Several of the times I brought very small children along with me because I had to. My husband wanted to come to POPL too, we couldn't just leave a one-year-old at home and I was breastfeeding. I found the community very supportive. It wasn’t difficult for me to arrange childcare. No one said anything negative to me about having a baby at a conference like POPL. I always felt like it was a welcoming environment.(Pictured on left: Stephanie with her husband Steve Zdancewic and their two children attending POPL 2008.)