Leo White on Language Design

Leo White — compiler engineer at Jane Street working on OCaml’s type system and language features — joins host Ron Minsky to explore the discipline of programming language design: why it resembles architecture more than science, how OCaml’s commitment to modularity shapes every feature added to it, and where the language must go to compete with C++ and Rust for low-level performance work.

Key ideas

1. Language design is a design discipline, not a science — closer to architecture than to controlled experiment. Running proper studies on programming languages requires professional programmers solving real problems in multiple languages over years, which never happens in practice. The useful analogies are architecture (constrained by mathematics, judged by how well people work in the resulting space) and mathematics itself (you can prove theorems and derive interesting properties, but no randomised control trial decides whether a building — or a language — is good).
2. OCaml’s modularity is a productive constraint that makes the language honest. Modules and functors (a module parameterised by another module — think of a function that takes a module in and produces a new one) force every language feature to declare its interface: you cannot add something to OCaml without specifying how it looks from the outside. This rules out Haskell-style type classes, which are inherently anti-modular — two libraries that independently define the same type-class instance cannot be linked together, because the type-class mechanism requires exactly one globally unique instance.
3. Evolving an existing language is harder and more valuable than designing a new one. A new language runs on easy mode: no backwards compatibility constraints, no existing users, no technical debt in the compiler. Real influence comes from working within an existing ecosystem, accepting that language design is a decades-long process, and learning from other communities’ failed experiments before importing the lesson into OCaml.
4. Mathematical simplicity in language features is not pointy-headed — it predicts composability. Languages with ‘sharp corners’ (C++ is the example) have features that interact in unpredictable ways; no two experts agree on which subset is safe. Mathematically grounded features tend to generalise beyond their original use cases — GADTs (generalised algebraic data types, an expressive extension of sum types) were added for compiler-writing and turned out to be useful for performance optimisation and memory-layout control in ways that surprised even the people who added them.
5. Dependent types are the natural destination of OCaml’s type-system ambitions. Right now OCaml programmers who want to track a property like ‘this file handle is read-only’ must invent a phantom type — a made-up type with no values, used purely to trick the type checker. Dependent types (types that depend on a value, not just other types) would let you write what you actually mean: a file handle indexed by an actual read/write enum. GADTs are a restricted, less complete approximation; dependent types complete the picture and eliminate the encoding errors that phantom-type tricks invite.

Content

Language design as architecture

White came to language design accidentally: as a Cambridge PhD student writing a C compiler in OCaml, he found a feature he wanted and, insufficiently supervised, added it to the language instead. Anil Madhavapeddy spotted the Cambridge address filing a type-system patch and recruited him to OCaml Labs.

The episode opens with the question of what programming language design actually is as a discipline. Minsky frames the problem: proper experiments would require professional programmers agreeing to use multiple languages on real problems over sustained periods, which has never happened. What runs in practice — studies of undergraduates in their first weeks — does not capture what anyone cares about.

White’s answer is that this is the wrong frame. Language design sits at the intersection of mathematics and aesthetics in the same way architecture does. You can prove useful theorems about your type system, just as a structural engineer can prove a building will not fall down; but whether the result is good to work in is a judgment, not a measurement. The academic community’s reluctance to discuss the aesthetic dimension in conference talks — even as it dominates hallway conversation — is, White suggests, a failure of the field’s self-understanding.

OCaml’s three defining properties

White identifies three features that make OCaml what it is.

Predictable performance. An experienced OCaml programmer shown a piece of code can reason about what assembly it will produce. This is not true of Haskell, where laziness — evaluating expressions only when their result is actually needed, rather than in the order they appear — means side effects could occur at any point, which forces the language into purity (no mutation, no I/O outside of explicit wrappers). OCaml is strict: expressions evaluate in the order they are written, which makes performance predictable.

A strong static type system. White notes that the type system changes how you write code subconsciously: he can feel when two variables of the same type are in scope, because that is a risk — he might confuse them. The type checker removes an entire class of mental overhead.

Modularity, taken seriously. OCaml has a separate language for describing interfaces, and functors allow you to write a module that is parameterised over another module — essentially, a function from module to module. This forces every feature to have an expressible interface. White compares laziness in Haskell to wearing a hair shirt: the discomfort of not knowing when evaluation happens forced Haskell to invest in purity, which was ultimately valuable. OCaml’s modularity plays the same role — it disciplines the language by ruling out features that cannot be cleanly abstracted.

The clearest illustration of what modularity rules out is type classes, the mechanism Haskell (and Rust’s trait system) use for operator overloading — allowing a single function name like + to work differently for integers, floats, and matrices. Type classes require that there be exactly one globally unique definition of, say, addition on integers across the entire linked program. Two libraries that each define their own addition instance cannot be combined. White’s research project, modular implicits, addresses this by removing the uniqueness requirement and reworking the search mechanism so it is grounded in OCaml’s module system rather than floating free.

Sharp corners and mathematical simplicity

The episode’s clearest argument for mathematically grounded language design comes through the contrast with C++. No two C++ experts agree on which subset of the language is safe to use — ‘it’s a really good language as long as you stick to a subset, but none of them agree on what the subset is.’ Features interact in surprising ways because they were added ad hoc, without a common mathematical foundation.

White reframes mathematical simplicity as compositional reasoning: if you can express formally how a language feature behaves, it is probably easier for programmers to reason about informally too. And features grounded in a clear mathematical story tend to generalise. GADTs — a type-system extension that originally seemed useful only for representing abstract syntax trees in compilers — turned out to be valuable for performance optimisation and memory layout control at Jane Street, in ways that surprised even the people who designed them. White, characteristically, suggests this confirms that all programming is secretly writing compilers.

The economics of language evolution

Writing a new language is easy mode; the hard, rewarding work is evolving an existing one. New features must compose with decades of prior decisions. Keyboards have a finite number of symbols. Technical debt accumulates in corners where someone took a shortcut. And language design is slow by necessity: a wrong decision is often effectively permanent, because the cost of a backwards-incompatible change scales with the size and reach of the codebase that depends on it.

White is sanguine about OCaml’s strategy of waiting for other language communities to attempt a feature, observe the failure modes, write the theory, and then import the best version. Type inference, garbage collection, algebraic data types (sum types — types that can hold either this or that, the obvious dual to structs that nobody has added to Go) all arrived in mainstream languages twenty or thirty years after their invention. OCaml sits in a position where it can seem simultaneously cutting-edge and stodgy depending on the frame.

Popularity, he notes, is ambiguous. More popular means harder to change incompatibly; it also means a richer library ecosystem and more review resources. His goal is not maximum adoption but a community large enough to be self-sustaining, and a language competitive enough with C++ and Rust for low-level performance work that Jane Street programmers are not forced outside it for systems code.

The performance gap and how to close it

The main gap between OCaml and C++ or Rust is control over memory layout. OCaml’s runtime is deliberately uniform: almost everything is either a tagged integer or a pointer to a heap-allocated block. This uniformity is what makes generic functions work without specialisation (any value fits in a single machine word), but the price is grotesque waste — a 32-bit integer requires a three-word heap block, and a stack-allocated struct is simply not available.

Three planned features address this. Unboxed types (similar to Haskell’s work on the same problem) let values like characters, 32-bit integers, and small structs live directly in registers or on the stack without any heap allocation. Local types allow safe stack allocation by marking functions as non-capturing — the compiler knows they will not store a reference beyond the call, so the caller can safely pass a stack-allocated value in without any Rust-style lifetime annotation appearing in the source. Resource management (closing files, database connections) is a third area where Rust’s ownership facilities would benefit OCaml, and White describes plans to import something equivalent.

Dependent types and the encoding problem

Much of the conversation about future type-system work circles around a recurring pattern: programmers who want to track a property statically — read versus write permission on a file handle, the length of a list — invent phantom types (made-up types with no values) to trick the type checker into enforcing the property. The encodings are error-prone and disconnected from the actual intention.

Dependent types — types whose definition depends on a runtime value — would let programmers write what they mean directly. A file handle could be indexed by a read/write enum that is a real value, not a fiction. A list could carry its length as a genuine natural number in its type. White sees this as a natural destination for OCaml’s type system, closely related to work already done on modular implicits and GADTs. Getting there is a large research problem — he spent two years proving a type system sound in the Coq theorem prover before touching the implementation — but he is optimistic about incremental progress in that direction.

Working with the upstream community

Jane Street started as a mere user of OCaml; eighteen years later it is among the language’s significant contributors, but it does not have the last word. The benefits of working with rather than forking the upstream project are real: review from developers who have maintained the compiler for thirty years, access to the full open-source library ecosystem, and the creative friction of having to explain why a feature belongs in the language at all. The cost is speed.

White describes the process improvements of recent years: moving from Mantis and SVN to GitHub pull requests, and creating an RFCs repository (Request for Comments — design documents submitted before the code is written, following Rust’s community practice) where design proposals can be discussed early. He is candid that Jane Street has not always communicated early enough, sometimes dropping a finished feature on upstream rather than sharing the work-in-progress design.

The episode ends with macros and algebraic effects. Algebraic effects — a mathematically clean mechanism for expressing concurrency, generators, and coroutines through a single language feature — are White’s example of a mathematically simple abstraction outperforming a collection of ad hoc ones: Haskell’s monads, Python’s async/await, Scheme’s continuations are all instances of the same underlying idea. Typed algebraic effects are the cleanest version, and the route to getting Racket-style compiler extensibility into a typed language — which White names as the field’s holy grail — runs directly through making type systems modular enough to accommodate user-defined language extensions.

Related

• Leo White — speaker
• Ron Minsky — host
• The Future of Software Engineering — theme; the conversation situates OCaml’s evolution within the broader question of what control programmers should have over runtime behaviour and what tools make large-scale software tractable
• Stephen Dolan on Memory Management, Garbage Collection, and OCaml — companion episode on the memory-management and unboxed-types work White discusses here