Pre-PLDI

It was another cold Ithaca morning. November 1st, 2012. All Saints Day, if that's your style, or All Hollows Day for the traditionalists. Either way, it was a day to remember.

I didn't know it right then. Woke up, like any other morning, scrambled out of bed and into a coat, and stumbled up the 40-degree, 900 foot incline separating my apartment from the university. That's Cornell for ya, Cornell in a nutshell. They say the hill's a metaphor; don't believe it. It's all part of the game, just another one of the little jokes we tell to survive the winter and isolation. You gotta forget the cold somehow.

My hands were still stinging from the frost when he walked through the door. Immediately, I knew something was up. Something was different. For starters, he was younger than you'd expect. Young for a professor. He was wearing a t-shirt, too. Beneath my double-layer coat, sweater, and long underwear I shivered a little on his behalf. Poor guy must've been from out of town. Then there was his computer, his slides. He didn't use powerpoint and he didn't use beamer. Instead, he projected a blank page on his tablet and scribbled notes with a stylus. Revolutionary. But most surprising were his feet. He wasn't wearing shoes.

The man was Ross Tate. The lecture was the Curry-Howard isomorphism. That summer I analyzed a mountain of code to see if one of his ideas held up in practice. It did, so together with PhD student Fabian Muelboeck we wrote it up in a paper. This summer, I'm fortunate enough to get to share this idea.

The paper is titled Getting F-Bounded Polymorphism into Shape and it's about an idea from Ross's friends in industry that has powerful consequences. They treated some classes/interfaces differently from others. Things like Comparable, Equatable, Addable, Clonable received special treatment in their codebase. Instead of being passed around as data or instantiated, they only modified other class/interface declarations. String, for example, might extend Comparable<String> to support a new method in type-safe way.

Ross determined the core rules influencing their guidelines. I did a survey of 60 java projects to determine whether other developers followed the same rules. It turns out they did. Ross then formalized these rules and made them part of the type system. Here's where the magic happens.

Just by separating these concepts--constraints vs. data--we eliminate cyclic dependencies in the type system. Immediately, subtyping becomes decidable under a simple algorithm. With a little more work, non-syntactic equality and decidable joins pop out. Future work is promising; in fact, I'm currently working on proving conditional inheritance in our system. It's one firm step towards a type safe world.

I'm glad to have gotten to work with Ross, and I'm grateful to be able to attend PLDI to share this idea with the community. Shouts out to PLDI, ACM SIGPLAN, and the NSF for making this happen.