Layout Polymorphism: Using static computation to allow efficient polymorphism over variable representations
In a small subset of the OCaml programs in use at Jane Street, the unpredictable latency induced by garbage collection is problematic. We are thus in the process of designing and implementing unboxed types for OCaml. These unboxed types can be created and manipulated without the need for allocation or the production of garbage.
However, all is not well. Heap-allocated types (along with int
) have a uniform representation, enabling polymorphic functions to work over any type even while the types themselves are erased. On the other hand, unboxed types come in a wide array of representations, thwarting parametric polymorphism. We dub the representation of an unboxed type its layout. This proposal describes an approach to layout polymorphism, allowing a function to work over a variety of representations. The underlying mechanism essentially echoes C++-style templates, requiring layout-polymorphic functions to be specialized at compile time. The innovation, however, is in continuing ML’s tradition of abstraction: in contrast to C++, we wish to type-check the layout-polymorphic functions before specializing, guaranteeing that the specialized version will run successfully.
The talk will describe our approach, including both type-system design (including a novel static mode) and implementation concerns around managing generating the specializations without interfering with separate compilation.
Layout Polymorphism (extended abstract) (layout-poly.pdf) | 410KiB |
Software Engineer at Jane Street. I believe that clever application of theory can eliminate a great deal of programmer errors – specifically, I think fancy types and functional programming are the future. I completed my PhD in 2016 at University of Pennsylvania working under Stephanie Weirich; my dissertation topic was the integration of dependent types into the Haskell programming language. I am a core contributor to the Glasgow Haskell Compiler (GHC) and Chair of the Board of Directors at the Haskell Foundation. My current work at Jane Street centers around further development of the OCaml language and compiler.
Fri 8 SepDisplayed time zone: Pacific Time (US & Canada) change
14:00 - 15:30 | |||
14:00 30mTalk | Programming with Explicit Effects in ReML Higher-order, Typed, Inferred, Strict: ML Family Workshop Martin Elsman University of Copenhagen, Denmark | ||
14:30 30mTalk | Wasocaml: a compiler from OCaml to WebAssembly (moved from OCaml workshop) Higher-order, Typed, Inferred, Strict: ML Family Workshop | ||
15:00 30mTalk | Layout Polymorphism: Using static computation to allow efficient polymorphism over variable representations Higher-order, Typed, Inferred, Strict: ML Family Workshop Richard A. Eisenberg Jane Street File Attached |