Share this Program

Copied!

We’re looking for type systems researchers to visit our OCaml Language 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, including unboxed types (avoiding allocation and improving cache locality), modes for data-race freedom, 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 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 over 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 start in a full-time faculty position, with your work here creating a natural bridge between your time in academia and your future as an 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:

• 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, 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.