Ron Minsky on Types and Why They Matter in Software

Jane Street uses OCaml for much of its work, but I do not think an applicant needs to arrive as a functional-programming expert or a trading specialist. Our software spans market data and trading, configuration, monitoring, research, clearing, distributed systems and security.

Tonight I want to discuss static and dynamic typing without making the familiar argument hotter than it needs to be. Choosing a programming language is difficult to settle scientifically: realistic questions concern difficult problems worked on by many people over years.

A study with students for a semester is much easier to run than randomly assigning experienced teams to languages for six years. My account therefore rests on experience and intuition; it has the biases of the work I have done, so take it with a grain of salt.

People often associate dynamic languages such as Python, Lisp and JavaScript with approachability and quick scripts, while seeing statically typed languages as serious, fast and sometimes unfriendly. Those categories contain very different languages, from Fortran and Java to OCaml, Haskell and Rust.

Fortran and Lisp go back to the 1950s. Fortran became associated with numerical performance, while Lisp gave early artificial-intelligence researchers flexibility. Those historical associations still influence how people think about languages.

A value is data that flows through a program: an integer, a string, a list or, in many languages, a function. A variable is a name for a value. The same variable can refer to different values in different calls or at different points in execution.

Variables are part of the program text; expressions combine variables and other syntax into computations. A type categorizes values, such as integers, strings and floating-point numbers. Even a dynamically typed language has types in that sense: its values have types.

In the contrast I am using, static typing also gives variables and expressions types. A typed variable’s constraint says what kind of value it can refer to across executions, and an expression such as x plus y has a type as well.

Historically, one purpose of types was performance. In Python, addition can mean integer addition, floating-point addition or string concatenation. A runtime has to determine which operation applies; if the compiler already knows the operands are integers, it can choose an appropriate machine operation.

Dynamic runtimes can work very hard to optimize frequent cases. A compiler can observe that operands are usually integers, check the assumption and use a fast path. In my experience, those optimizations can be brittle, making performance less predictable when code changes.

Types also help people understand programs. They can tell the programmer and collaborators what kind of data flows through a function. That benefit sits alongside performance, but neither means there are no costs.

Typed programs can be more verbose. To make that concrete, consider a small function that takes a floating-point number and returns its integer part and the remainder. In Python it fits into a short function returning a pair.

In early Java, there was no general-purpose pair with independently varying element types, so expressing the result required a new class, constructor and accessors. Later Java generics allowed a reusable pair, making this example shorter.

The expressiveness of a type system affects how much extra code you write. When a natural structure cannot be expressed directly, programmers may need an awkward substitute. Better abstractions can reduce the gap, though they do not erase every trade-off.

OCaml’s implementation of the same function is also compact. Type inference lets the compiler derive the function’s type from its operations, so the programmer need not annotate every variable. An editor can still show that it accepts a float and returns an integer and a float.

Inference and expressive types mitigate verbosity, but typed languages can still require explicit information. They also add something to learn: programmers must understand both the computations and the constraints that the type system imposes on them.

Consider asking for the length of a list. Python provides a general length function and gives an error if asked for the length of an integer. OCaml typically uses functions such as List.length and String.length, which requires a little more specificity.

Haskell offers a more general length function over foldable structures. That generality is useful, but the type and error messages can be harder to interpret. Different type systems occupy different positions between expressive power and conceptual complexity.

Finding a useful balance is a language-design problem. A system should be expressive enough for concise programs while remaining understandable, including when it explains why a program fails to type-check. Some languages make this balance easier than others.

Types can slow down a small task. Writing a short Python program may be quicker than thinking through the corresponding types in OCaml. A type system can also interfere with a design when it cannot naturally express what the programmer wants to do.

That cost varies by language and task. Some experienced programmers deliberately choose dynamic languages for certain work because they open up a design space that is cumbersome to express in a particular static type system. It is a real trade-off.

My positive case for types begins with performance, but error detection matters too. People sometimes judge types by a relatively limited system and underestimate what a richer one can express. In languages such as OCaml, ordinary null-pointer errors are avoided through a different treatment of absence.

Take a function that compares two dictionaries and reports keys present in both whose values differ. A Python version mistakenly reports a key found only in the first dictionary: the second lookup returns None, which is then compared with the existing value.

That looks like a logic mistake rather than the stereotypical error of passing a float where an integer is expected. In the OCaml version, however, the lookup returns an option. Comparing that option directly with an integer fails to type-check.

The correction is to match the two cases: if the lookup returns None, do nothing; if it returns Some value, compare that value. The type makes the possibility of absence explicit and forces this part of the program to confront it.

The small example cannot demonstrate every benefit of working at scale, but it shows that a useful type system can catch more than mismatched primitive types. With careful design it can reveal errors about the meaning and structure of a computation.

A type signature also communicates information. Unlike ordinary prose documentation, the type is checked against the program, so it does not quietly drift in the same way when code changes. More informative types can communicate more of the structure that users need.

Types can guide refactoring. Change one part of a system and the checker points to other parts that no longer fit. Interns sometimes find it surprising that after making substantial changes and following the resulting errors, their program still works.

Not every type system supports this equally well. Types can also encode invariants: facts that should stay true as a program evolves. When a computer can check those facts, programmers can spend more attention on problems the computer cannot check for them.

Tools benefit from type information too. A tool that understands the shape of a program can provide navigation, completion and other help to the programmer. This is one reason types have gained traction in the JavaScript ecosystem.

Do not judge all type systems by the weakest example you have encountered. Python versus Java is not the whole design space. Explore other languages, but remember that a fast, accessible script and a large, correctness-sensitive system may call for different choices.

Asked about evidence, I would not claim expertise as a social scientist. Mining open-source repositories may yield useful clues about real work, but language choice is not randomly distributed across projects or programmers. Those selection effects are hard to correct.

Studies of beginner mistakes can also lead to different conclusions from the needs of experienced programmers. A diagnostic that suggests undoing the smallest change may be sensible for a novice, while an experienced developer may have made that change deliberately and want guidance on updating the rest.

Among features I particularly value is type inference: it removes friction while retaining the other benefits of a type system. Inference has become more common across languages, including forms of it in C++ and C#.

Another is the algebraic data type, especially the sum type. A product type combines fields: this and that. A sum type describes alternatives: this or that. Together with exhaustive case analysis, it offers a direct way to model different possibilities.

Good language ideas can take a long time to reach the mainstream. Garbage collection existed decades before it became common in mainstream languages. In 2017, I thought sum types were similarly underused, despite their practical value.

Asked how Jane Street’s OCaml practice has changed, I would start with the language itself. First-class modules let us take the module system’s units and interfaces and pass modules to functions or store them in data structures, enabling cleaner modular programs.

Generalized algebraic data types, or GADTs, also proved useful in ways we had not anticipated. They looked like a feature mainly for compiler writers, yet we found them valuable in systems programming and in high-performance code that needs control over memory layout.

We have also improved at type-directed design: putting more invariants and structure into library interfaces so that they are easier to understand, use correctly and change. A restriction can be seen as shared knowledge about how a library is meant to be used.

Our early OCaml systems were small enough to build even though I had much to learn. As the organization grew, the relative obscurity of the language brought costs. We invested in documentation, editor features, the compiler and optimization, including a dedicated tools and compilers group.

I would welcome a mainstream language with these features that was not shaped so heavily by a collision with a legacy ecosystem. Scala, F# and Swift combine ideas from different worlds. Their integration offers benefits, but the combination can add complexity.

OCaml’s relative independence gives it a simpler design in my view, with Unix and C integration rather than deep integration into a large managed ecosystem. That choice has a cost too: there are obvious benefits to being inside an ecosystem such as the JVM.

For a high-throughput packet-processing system, imagine a memory region receiving data directly from a network card. The program reads bits, mutates structures and repeats, without allocating a new object for every message. The challenge is to make that low-level shape pleasant to program against.

GADTs can let the program refine what it knows: first that bytes contain a TCP packet, then that the packet contains a Nasdaq message, and then that the message represents an add order. The interface can feel like a hierarchy of alternatives and combined fields while avoiding the allocations that a conventional representation might require.

Gradual typing raises a related design challenge: how do you add static checks to an existing dynamic language while preserving its idioms? The result has to reconcile two styles, and the details can become complicated.

Typed Racket is an impressive example. Racket has a numeric tower in which arithmetic naturally moves among integers, large integers, rationals and complex numbers. A type system that models those behaviors precisely can become extremely elaborate, including many distinctions among numeric cases.

Static type systems are conservative approximations, so some dynamic-language idioms do not fit easily. Some gradual systems deliberately accept unsoundness to make adoption and tooling easier. That is a consequential compromise: if a compiler cannot trust a type claim, it cannot safely rely on it in the same way for optimization.

My own rule of thumb is that typed languages can slow you down in the small and speed you up in the large. Jane Street also spends time on review and quality control, especially for software that can send orders to exchanges. That is a separate, deliberate trade-off in favor of correctness.

For a short trading competition, where a participant has perhaps 12 hours to build a prototype against a simulated exchange, I would often recommend Python. For Jane Street’s longer-lived systems, the choice I faced was largely between Java and OCaml, and I found OCaml faster and easier for that work.

Types do not replace tests. They can catch some errors automatically and reduce the number of cases that must be checked by hand, but important behavior still requires testing. At Jane Street we have invested in making testing infrastructure easier to use, because friction discourages necessary work.

For some simple, well-typed programs, a few examples can appear to make the behavior snap into place. That is not proof that all bugs have disappeared. Rather, types can constrain behavior enough that well-chosen tests become more effective.

One common invariant concerns dependencies between fields. If an object’s tag says it is case A, one field may need to be populated; in case B a different field is required. Product types alone cannot express every such relationship cleanly, but a sum type can tie each alternative to the data it requires.

Those data constraints can represent facts about program state too: for example, a particular state may require that a session identifier has already been established. Encoding the relationship reduces the amount of coordination that must be maintained by hand.

Another example is distinguishing untrusted user input from a string that has been quoted for a database. Separate abstract types can require an explicit conversion before a function expecting quoted data accepts it. The checker then helps track the required property across the program. This example illustrates a type-level invariant; safe database access still depends on using the appropriate query and escaping mechanisms correctly.