Share this Program

Copied!

We’re looking for type systems researchers to visit our compilers team. You’ll work on the design, implementation, and formalization of OCaml extensions we’ve been building. This is an opportunity to see how programming language concepts can be put into practice in the hands of a large and expert team of functional programmers.

There are a bunch of ambitious changes to OCaml that we’re somewhere between dreaming up and implementing, notably: stack-allocated values (avoiding garbage collection), unboxed types (avoiding allocation of any kind), and modes for data-race freedom. We’re looking for help in working out the full, formal implications of these designs — and in sharing these innovations with the world via peer-reviewed publications in top venues. Along the way, we’d expect that work to uncover new opportunities for us to improve the design and implementation of these features, guiding the future of OCaml and advancing the state of the art on practical type-systems work.

The ideal candidate will have a faculty offer in hand and will delay their start at a top research university in order to work with us for one year. We are also open to evaluating excellent candidates looking for a more typical postdoctoral appointment, for up to two years.

As a visiting researcher, you’d get to witness how we develop a language feature from conception to deployment. Because we have a large community of internal users, we have the unique ability to quickly iterate on language features after they’ve been released, incorporating feedback from early adopters. We hope your experiences here will inspire further research after you start in a full-time faculty position, with your work here easing the difficult transition from graduate student to independent researcher. On our end, we’re looking forward to continuing our relationship well past the one or two years we spend together, seeking ongoing collaboration with you as you develop your career. We’re also excited to share ideas back to the research community that has given us so much.

Are you interested in other program opportunities for Visiting Researchers?

Here are some projects that we think would be natural areas to collaborate on:

• Locality. Jane Street has enhanced OCaml’s type system with the ability to track locality of data. Values have a mode, which may be “local” or “global”, and local values are not allowed to escape the current dynamic region (such as a function body). Our original motivation was performance: we’ve modified the OCaml runtime to allocate local values on the stack, avoiding garbage collection overhead. But we’ve also found surprising benefits for expressiveness and reasoning. For example, functions which take local arguments are guaranteed not to capture them, allowing us to build safe APIs for things like temporary file handles or GPU memory. We believe the core innovations here can benefit other languages, and there may be unseen opportunities for improvement. A visiting researcher might work with our team to formalize and publish these designs.
• Layout polymorphism. Jane Street is currently in the middle of a multi-year design and implementation effort to create unboxed types in OCaml. The key challenge is to integrate types with a variety of runtime representations with type-erasing parametric polymorphism. Our solution is to create a system of layouts, where a type is classified by a layout that describes the representation of its values. (Layouts are similar to kinds in other languages.) However, we now must confront the next problem: how to get functions to be polymorphic over layouts, not just types; such functions would need to be able to work on values with a variety of runtime representations. Achieving this goal without sacrificing efficiency (and without doing any runtime code generation) is a challenge; our initial approach includes an analysis of the user’s program to identify statically known values, which can be used to specialize layout-polymorphic functions at compile time. A visiting researcher might flesh out (or replace!) this design and could lead the implementation and deployment of this large new feature, alongside writing up and submitting the work for peer-reviewed publication.
• Data-race freedom. OCaml 5 supports multi-threaded programming, an essential feature for today’s multi-core processors. However, multi-threading comes with a grave danger: data races. Jane Street is currently working out a design for data-race freedom via a system of modes (not unlike Rust’s ability to track ownership). We’re confident (but haven’t proven) that the core approach avoids data races, but it’s not yet clear whether it strikes the right balance of expressiveness and safety. For example, we want to allow a logging facility to be shared among threads, even though doing so might lead to non-determinism in the logs, which the current approach makes difficult. Or we might want to build standard synchronization primitives on top of unsafe features. You would contribute to this design a way to be sure we avoid data races while still allowing the expressiveness modern programmers expect from a multi-threaded language. We expect this work to form the basis for a submission for peer-reviewed publication.
• But wait, there’s more! The type systems team is hard at work on other aspects of the language as well, including a way to track the ability to mode-cross via a kind system, support for mode polymorphism, and novel approaches to unboxed types (including support for unboxed sums). You would be invited to contribute to these projects as well, looking for opportunities to connect this work with the wider research community. In addition, a researcher interested in evaluation could develop protocols for measuring the impact of all of these improvements within Jane Street’s codebase.

We expect this position to be based in our New York office, supervised by Dr. Richard Eisenberg, though we would also be happy to hear from compelling applicants who would work in our London office.

If you’re interested, let us know

Please fill out this form to express interest. Don’t worry too much about every little detail. It’s an informal process, and we expect to tailor the program to each individual. We’ll be in touch if it sounds like there could be a good fit.