dress shoe
bare foot
 Ross Tate

Ross Tate

ROT13("pbagnpg@ebffgngr.bet")

Researcher and Consultant

Programming-Language Design and Implementation

Computer Science Ph.D. at University of California, San Diego [Thesis]
Mathematics & Computer Science B.S.s at Cal Poly, San Luis Obispo

Before Kotlin was released, I worked with Andrey Breslav to design its type system. In particular, we focused on how to design the bridge between the type system Kotlin wanted to have and the type system it needed to interoperate with: Java. The two main challanges were nullability and wildcards. For nullability, I designed the ! operator, a form of sound gradual typing that lets Kotlin programmers "optimistically" treat Java values as non-null while also informing the compiler where to insert run-time checks. For wildcards, I designed mixed-site variance, which lets Kotlin programmers combine Kotlin's declaration-site variance with Java's use-site variance (encoded as wildcards). Thus I designed Kotlin's platform types that proved critical to its initial adoption.

Java is one of the most thoroughly studied programming languages. Yet, despite many years of academic verification, I discovered that Java's type system is unsound—even without using backdoors like raw types or covariant arrays, you can trick the type system into believing a String object is an Integer object. It turns out that everyone had overlooked null pointers! As another problem, Java subtyping is undecidable. While that is not my discovery, my students and I discovered why this does not affect programmers in practice. In particular, even though programmers have had access to the full expressiveness of F-bounded polymorphism (i.e. recursive type constraints) for over a decade, programmers only ever used it to encode particular patterns akin to Haskell's type classes. I proved that, because real Java programs conform to material-shape separation, the standard subtyping algorithm is actually complete in practice.

The discovery of Java's unsoundness actually started with Scala. Back when she was developing the core calculus for Scala, Nada Amin and I discovered that the calculus would be unsound if extended with null pointers. Since Scala already had null pointers and all of the features of the calculus, we were quickly able to develop an unsound Scala program, and Nada created an unsound playground where you can play with these and try to make your own examples.

Now just a part of history, the Ceylon programming language—led by Gavin King at Red Hat—began development back when there was a massive gap between Java and Scala (and before Kotlin was around). The team was developing a next-generation object-oriented industry-scale programming language, attempting to incorporate all the experience offered by languages such as Java, C#, Scala, Smalltalk, and Python over the last decade or so. My role on the team was primarily as type-system advisor, making sure Ceylon's powerful features all worked together cohesively. Although it failed to achieve widespread adoption, many of its features—particularly of its type system—would find there way into other major languages, notably Java, Scala, and Kotlin.

Along with Jan Vitek and his research group, I have been working with the Julia language team to fix issues with the run-time type system. In particular, we determined that Julia's subtyping system, which is used at run time to determine which method a function call resolves to, is undecidable. This means it is impossible to implement Julia's runtime correctly. So we analyzed Julia programs and determined a restriction on types that real programs already conform to and yet exhibit an innate hierarchical structure that makes them much easier to work with. With that pragmatic structure on place, we are developing an improved subtyping algorithm capable of completely handling the entirety of Julia's rich feature set.

My contributions above have all been for user-facing languages. But user-facing languages are compiled to low-level languages. While working with Juan Chen and Chris Hawblitzel at Microsoft Research in Redmond, I designed an inferable typed variant of x86 that an operating system or virtual machine could independently validate to ensure the program was memory safe. We ensured this could support all compiled C# programs, even with C#'s support for many low-level representation and execution optimizations. We even supported nearly all optimizations existing C# compilers employed, and as such our typed assembly had low-percentage overhead relative to raw compiled x86 programs.

WebAssembly is a web standard for a low-level language. Unfortunately, it is nowhere near as efficient as a typed assembly language, with many language teams finding their WebAssembly programs are multiple times slower than their native counterparts. So I have been working with the standards committee to integrate insights from typed assembly languages and to broaden understanding of the wide range of low-level techniques that various programming languages need WebAssembly to support in order to perform well.

Ross Tate has made fundamental contributions to type systems with applications to OO languages. This includes the discovery that although wildcards as in Java are undecidable in theory, programmers only use specific flavors of wildcards which keeps them decidable in practice (PLDI'11); similarly, he proposed that F-bounded polymorphism can be replaced by simpler concepts, which were sufficient for the use that programmers made of generics in a large corpus (PLDI'14). Finally, he discovered that Java wildcards and Scala path-dependent types, in combination with implicit null pointers, make the languages unsound (OOPSLA'16). In addition, he has had strong industrial impact via his involvement in the production languages Ceylon (Red Hat) and Kotlin (JetBrains).

Former Students

Former Advisors

Graduate
Sorin Lerner
Undergraduate
Aaron Keen

Awards

Publications

Professorship

I was an Assistant Professor at Cornell University for many years. Besides research and teaching, I am proud of the impact I had on many campus communities. At the graduate level, I fostered regular social events between students, staff, and faculty across the College of Computer and Information Science to form better relationships across these groups. At the undergraduate level, I worked with undergraduates to address issues with elitism, sexism, and racism. In particular, I worked with students to organize large student body community discussions of its issues, helping students see they were not alone in their struggles, raising broader awareness of the issues, and working together to identify changes we could make as a community and individually to improve the circumstances. I was honored to be invited to serve on the newly formed Women in Computing at Cornell's Faculty Board, and to moderate student discussions for Cornell's former Tapestry of Possibilities: Diversity at Cornell program. Finally, though most of the credit goes by far to the student organizers, Junia George and Leon Zaruvinsky, and department event coordinator, Jessie White, I helped start—and maintained for many years—Cornell's main hackathon: BigRed//Hacks.

Ross Tate Capoeira

Classes

Research Internships

I interned under Daan Leijen at Microsoft Research in Redmond in Summer/Fall 2009. We designed a pure but effectful functional programming language, as well as a Hindley-Milner-like type inference algorithm with effects and higher-order polymorphism (based on Daan's HMF). In doing so, I improved compiler technology for inferring higher-ranked polymorphism. I also managed to generalize monads in order to formalize effect systems with multiple interacting effects.

I interned under Juan Chen and Chris Hawblitzel at Microsoft Research in Redmond in Summer/Fall 2008. I designed a type-inference algorithm for an x86 assembly type system for object-oriented programs, as can be seen at PLDI 2010. This typed assembly language, which we called iTalX, is now a key part of Microsoft Research's computer-verified memory-safe operating system, Verve. In order to design this inferable type system, I first designed a framework for existential types based on category theory, which has proven to be intuitive, powerful, and flexible. This framework was then reused for my work on Java's wildcards in PLDI 2011.

Industry Internships

I interned at Treyarch, a studio of Activision, twice. The first time I worked on the early stages of the Spider-Man 3 console game. The second time I worked on Spider-Man: Web of Shadows. My biggest contributions were in improving the scripting language used by the game designers, and this may have somewhat fostered my enjoyment of programming languages. I also worked a lot with computational geometry and corresponding graph theory.

Before that, I interned at CustomFlix. At the time, CustomFlix was a very small internet company which processed, distributed, and marketed personal videos. I held various roles such as architect, tester, lead, and web developer.

Post Script

I originally stole this site design from Patrick "Maxim" Rondon, which Stephen Longfield then stole from me, though all our designs have changed since.

Before I made this site, searching my name would pull up this page about my grandfather.