There are a bunch of ambitious changes to OCaml that we're somewhere between dreaming up and implementing, including unboxed types (avoiding allocation and improving cache locality), modes for data-race freedom and purity, and representation polymorphism (the ability to write one function that works efficiently over many different runtime representations, without indirection) – all while retaining backward compatibility and preserving ease of use. 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 either be a professor or 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'll get to witness how we develop a language feature from conception to deployment. With 1,000+ 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 leave Jane Street. On our end, we're looking forward to continuing our relationship well past the time we spend together, seeking ongoing collaboration with you. We're also excited to share ideas back to the research community that has given us so much.

Here are some projects where we think there are natural opportunities for collaboration:

• Representation 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.
• Mode inference. As described in our recent POPL paper, our branch of OCaml already supports a type system feature (called modes) that guarantees data-race freedom. But these modes can sometimes be onerous to work with. We currently have ideas for how to improve upon the status quo, in two different ways:
  • We can use the kind system (every type is classified by a kind) to track which types do not care about a certain mode. (For example, deeply immutable data types never care about whether they are contended – that is, accessible from multiple threads.) When a type does not care about a mode, values of that type can freely be coerced to have a different mode than the one originally inferred; this is an important feature for usability of the mode system. However, what do we do about parameterized types? After all, an immutable list can ignore contention exactly as much as the data it contains. This has led us to design a novel form of kind polymorphism for such structures. Yet we are increasingly discovering unfinished business in this area: How should the new design fully accommodate GADTs? How do we infer the right kind for irregularly-recursive data types? How do we efficiently compute the subkinding relation? These are all open questions you might be able to help us consider.
  • In our current design, we allow the embedding of data with one mode inside of structures with a different mode by way of a modality. (These modalities are often rendered as a little prefix square before a type in many papers.) The modalities must today be written explicitly, with manual injections and projections. Yet we think it should be possible to infer the uses of these modalities, making programming with modes significantly easier. Perhaps you could help flesh out the details here and even implement the new scheme.
• But wait, there's more! The type systems team is hard at work on other aspects of the language as well, including support for mode polymorphism, novel approaches to unboxed types (including support for unboxed sums), and support for metaprogramming with compile-time evaluation. 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, working alongside 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, please fill out this form. 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.