Richard Eisenberg on Dependent Types, OCaml, and AI-Assisted Programming

Ron Minsky introduces Richard Eisenberg, a senior contributor to Haskell, member of the GHC steering committee and chair of the Haskell Foundation. Eisenberg has joined Jane Street's tools and compilers team to work on the OCaml compiler front end.

Eisenberg first encountered Haskell as he prepared for graduate work in programming languages after teaching high school. Learning about dependent types astonished him: a sufficiently expressive type can describe an intended program before implementation, letting the compiler check whether the implementation meets it.

Asked for an accessible explanation, Eisenberg begins with the effect rather than the definition. A language with dependent types can encode a proof of correctness in a program and check that proof each time the program is compiled, provided the specification has been set up appropriately.

Consider sorting a list of integers. A function from a list of integers to a list of integers is too weak a description. Requiring the output to be in nondecreasing order is better, but a function that always returns the empty list would still satisfy it.

A more complete specification says the output must be both nondecreasing and a permutation of the input. Different sorting algorithms can meet that same type, and the compiler can check their proofs. The type is dependent because the required output depends on the particular input.

Haskell did not yet have full dependent types, but its expressive type system attracted Eisenberg. At the University of Pennsylvania, he worked with Stephanie Weirich and then Simon Peyton Jones, beginning a collaboration on Haskell and its compiler.

His interest in languages began much earlier. He learned BASIC as a child and acquired a Pascal compiler around age twelve. Assuming the manuals contained everything he needed, he spent hours deciphering syntax diagrams and taught himself to program from them.

A programming languages course taught by Norman Ramsey later rekindled that interest. Eisenberg taught high school before returning for a PhD. During that work, he wanted compiler support for an idea about dependent types; Peyton Jones encouraged him to implement it himself, with mentoring from both collaborators.

At Bryn Mawr College, Eisenberg could count open-source contributions alongside scholarly publications. That allowed him to continue compiler work while researching and teaching, but maintaining all three was demanding. After years of teaching, he decided to move in a different direction.

He joined Tweag, a software consultancy, to continue Haskell research and compiler contributions. Later he wanted to work on a cohesive team and see another language. Minsky's invitation to Jane Street eventually arrived at the right time, although the process took about eleven months.

Eisenberg initially hesitated over his impressions of the financial industry and commuting to New York. He found the role appealing because it includes work on an open language and contributions to a wider ecosystem, continuing research interests he had developed over the preceding decade.

Minsky returns to the practical cost of dependent types. Proofs can be hard to construct, and theorem-proving systems require substantial engineering. If proofs become part of ordinary programming, he asks, can the process be convenient enough without disrupting everything else?

Eisenberg says the community is still grappling with this question. His principle is that the more advanced features should be opt-in: even in languages supporting dependent types, a programmer should be able to write a simple list-to-list sorting function without proving every property.

The decision to prove a property is a cost-benefit judgment. Proofs take effort, but for an important and error-prone component they may reduce testing, debugging, or the risk of a serious failure. Experience and judgment determine where the additional assurance is worthwhile.

Minsky describes this as paying as you go: start with a relatively simple language and add power when needed, without forcing complexity into every task. Eisenberg agrees that making this boundary work is difficult; his Haskell work aims to add dependent-type features while preserving simple programs.

At Jane Street, Eisenberg's broader goal is to use types to structure thought and programs. A specification can clarify an intention before implementation and let the compiler check it. Ideally, that checking happens at compile time rather than imposing a cost on users at runtime.

His concrete project is unboxed types. Imagine a trade record nested inside other structures: with a naive boxed representation, accessing an inner field can require following several pointers, with potential cache misses. The aim is to support useful type structure without requiring that chain of allocations and indirections.

Minsky explains that OCaml's traditional representation is deliberately simple: values are generally immediate machine-word-sized values or heap-allocated blocks with a header and word-sized slots. Eisenberg sees the resulting runtime cost of some type structure as a language-design problem.

Minsky clarifies that unboxed types do not make performance details disappear. Instead, they make certain representation choices explicit at the type level. Eisenberg agrees: execution still has a physical model, and programmers need enough information to design fast representations.

Minsky contrasts automatic optimization with performance engineering. A compiler improvement that speeds most programs by 20% is a huge general win, whereas giving a programmer precise control can sometimes make a particular program five, ten, or even a hundred times faster. Both approaches matter, but operate at different scales.

Eisenberg sees a continuing tension between abstraction and control. High-level languages spare programmers from writing every machine instruction, but hiding too many execution details can prevent performance engineering. The compiler should use a small number of useful hints to generate efficient code without exposing every low-level detail.

The same pay-as-you-go challenge appears in unboxed types. Eisenberg explains that they can interfere with polymorphism: a generic list-length function relies on a type variable that can stand for many element types, but some unboxed representations do not fit the same uniform assumptions.

The team must find ways to preserve useful polymorphic algorithms despite varying physical layouts. As they experiment, they expect to find programming patterns that no longer work and devise ways around them. Code generation is one possible part of the solution.

Minsky explains the mechanical issue: with a uniform boxed list representation, one piece of code can traverse nodes of the same shape. Different unboxed layouts may require different machine instructions, so restoring polymorphism may require generating code for multiple representations.

Eisenberg says their best idea at the time is to generate the necessary code at compile time. That could rule out some potential idioms, though he expects few practical users to need them. The design remains difficult, and the team still needs experience with it.

Minsky compares the project with Rust, which combines type safety and control over low-level memory. Eisenberg highlights a major difference: Rust gives up garbage collection. For many programs, including compiler code where microsecond latency is not critical, automatic reclamation is extremely convenient.

Rust's memory model asks programmers to consider allocation and deallocation throughout the program. Eisenberg wants OCaml to retain its garbage-collected model for most applications while offering finer control where it is needed. In that sense, the team is trying to preserve the pay-as-you-go principle.

Minsky questions whether paying as you go is always best. Gradual type systems can gain complexity from mixing typed and untyped code; sometimes a uniform choice, such as using types throughout a language, is simpler. For certain applications, explicit memory control everywhere may likewise be desirable.

Eisenberg reframes the goal as multiple modes with easy interoperability. One file or package could use ordinary OCaml memory representation while another requests tighter control. Polyglot systems address a similar need, although connecting languages can be difficult and each pairing brings its own issues.

One possible design makes boxing an explicit operation, inserted automatically for ordinary code. A compiler setting might turn off automatic boxing so every allocation must be requested explicitly. Eisenberg stresses that this was an idea for experimentation, not a settled design, and garbage collection would still remain.

Minsky notes that Jane Street does not own OCaml and must persuade upstream maintainers to accept changes. Eisenberg sees that relationship as a benefit. OCaml began at Inria, and Jane Street both benefits from the community's work and contributes ideas back to it.

The team can experiment internally, gain confidence in a design, and then work with the broader community to see whether it belongs in OCaml for everyone. Eisenberg cites OCaml 5 multicore support as substantial work largely outside Jane Street from which the company can benefit.

Open collaboration also improves individual changes: Eisenberg describes sending a compiler improvement upstream and receiving a better idea from someone outside the firm. Minsky contrasts this workflow with Haskell development, where early design and evaluation were more deeply integrated with the open-source community.

Eisenberg says an internal environment enables experiments before a language feature reaches thousands of users. Once a public feature is widely used, changing even a flawed design can break programs: users who dislike the feature may still rely on it, and others may value it highly.

At Jane Street, engineers can introduce a feature, learn from internal use, and make coordinated repository-wide changes. A 'tree smash' can update code together. He gives local types and stack allocation as an example of a design being revised after use, before upstreaming.

Minsky asks whether internal testing risks overfitting features to Jane Street's unusual needs. Eisenberg agrees that it is a real concern. The team seeks public feedback early, including community presentations on unboxed types and local allocation, to test whether the ideas have wider value.

Eisenberg remains active in Haskell while learning OCaml. One difference he notices is where interfaces live: Haskell programmers commonly put type signatures next to functions, whereas OCaml often separates a module's interface into another file. He suspects this affects documentation habits.

Haskell's type classes let one function name stand for several operations, which can make a chain of expressions harder to interpret. OCaml tends to be more explicit about the operations at runtime. Eisenberg generalizes cautiously: Haskell often exposes more at compile time, OCaml more at runtime.

Lazy evaluation is another distinction. Haskell can defer a computation until its value is needed, potentially avoiding work but making performance harder to predict. OCaml generally evaluates the computation immediately, making the rough execution order easier to read from the code.

Minsky questions whether differences in annotation and documentation come from the languages or their cultures. OCaml permits more annotations, and interface files are a natural place for comments. Eisenberg acknowledges that his impression may be biased by comparing the two compilers, whose old code predates current programming practices.

The two languages also approach extensions differently. Minsky describes OCaml as relatively conservative and Haskell as more experimental, with features enabled through pragmas. Eisenberg says GHC had around 150 extensions when he last counted, creating a vast theoretical configuration space.

Eisenberg traces this to Haskell's history as a standard implemented by several compilers. Extensions let implementations experiment while retaining a shared core. OCaml instead has a language manual and a primary implementation, rather than the same standard-and-multiple-compiler structure.

With GHC now dominant, Eisenberg finds the old extension system less well motivated. Users may need long lists of flags, and newcomers cannot easily distinguish mature, experimental, and problematic extensions. The GHC steering committee is discussing a more approachable organization that preserves backward compatibility.

Eisenberg would like a more unified standard language, perhaps reducing the effective choice from roughly 150 extensions to a handful. He does not expect to eliminate extensions entirely: Haskell serves too many use cases, and removing the mechanism outright could divide the community.

Minsky turns to AI-assisted programming. Eisenberg sees it as a significant step, but not an end to programming-language design. A programming language is a medium for precise communication between humans and computers, and between humans; generated code adds communication from computer back to human.

Humans still need to read generated code and decide whether it does what they intended. Eisenberg has long favored optimizing language design for reading rather than writing: a concise symbol may be clever, but a word can be easier to search, learn, and understand.

If computers write more code and humans write less, the pressure for readability increases. Future representations might become richer and more structured, but Eisenberg views this as another phase in the evolution of precise communication, rather than a reason to discard everything and start again.

Dependent types could supply precise specifications for AI-generated implementations. The sorting example illustrates why wording matters: the output must be a permutation of the input in nondecreasing order, including duplicates. A model could generate code against that specification, and the result could be checked.

Minsky is skeptical that people will routinely write precise specifications because they are hard, and suggests asking a model to draft one for a human to review. Eisenberg agrees that drafting is difficult but warns that the human must still understand and validate the specification; otherwise the system has lost its connection to the intended result.

Minsky observes that reading is hard too. In code review, a valuable exchange often begins when a reviewer cannot understand a messy implementation and asks for simplification. It remains an open question whether AI assistants can produce code that is genuinely easy to understand.

Eisenberg adds that if a simple, precise specification can be checked tightly against an implementation, the implementation's simplicity may matter less to correctness. Dependent types are one possible mechanism; refinement types and other approaches can also connect a specification to an implementation.

The two discuss languages as intermediate representations for working with AI assistants and building confidence in results. Eisenberg thinks it was too early, after only a few months of rapidly changing interactions, to design a language from scratch around them. Existing languages remain a useful starting point because they already support precise communication.