I have, for a few years now, thought about how to show type errors to developers. Earlier this year at the MIT Programming Language Review I gave an iteration of my talk on Argus, an interactive debugger for Rust trait errors. In this talk I claim that static, textual error messages are the wrong medium for communicating errors.
The reason static text is a poor medium is it requires you to print all information up-front. Compilers need to determine what is essential to print for an error, throwing away information that might be useful but would ultimately make diagnostics too verbose. It’s also bad because you may want to provide hyperlinks, colored text, and other niceties for reading.Some of these are available in modern terminal emulators, but are not guarateed everywhere, e.g., GitHub action workflows.
The past summer I spent some time thinking about error messages for OxCaml, Jane Street’s branch of OCaml. OxCaml and Rust have a common theme: members of the target audience for the language don’t understand the langauge’s theory. I.e., if you’re trying to use Rust, you might not 100% understand ownership. If you’re trying to use OxCaml, you might not 100% understand modal type systems. Advanced PL-theory shouldn’t be a barrier for entry for any programming language; you should be able to program in Rust without being an ownership wizard and you should be able to program in OxCaml even if you know only OCaml.Some functional programming knowledge is required.
One way to achieve my goal is to bootstrap people into the language’s ideology using educational diagnostics. In this world, diagnostics carry the burden of doing some lightweight introduction and education on language-specific terms and concepts. Of course good documentation is still necessary and educational diagnostics can even provide links to relevant documentation sections!
The problem I realized is that, in many languages, typechecking and diagnostic rendering are coupled around the fact that diagnostics are text-based. This really frustrates me. Diagnostics can be so much more than text, for not that much more work. Creating an alternative view of diagnostics for OxCaml or Rust is (currently) an enormous amount of work, because I need to modify typechecking, expose functions and state, thread information around where it wasn’t going etc. In this post I want to motivate the idea of parametric error rendering, or simply, the ability to experiment with alternative diagnostic forms for cheap.
Now comes the fun part. To motivate different styles of diagnostic, we’re going to look at errors from a researchy langauge. I’ve built an OCaml-like language that combines polymorphism and subtyping. You shouldn’t need to know what any of those words mean in order to debug an ill-typed program. The language is called Howl—for no particular reason.It’s a variant of Stephen Dolan’s MLsub for those that care. We’re going to look at several iterations of diagnostic, that provide increasing amounts of information.
We will start how all languages do, using simple textual strings as a diagnostic medium. Below is an editor pre-loaded with our running example. There is a “distilled” form of the program to keep things simple, and there’s an “expanded” form of the program for something that resembles how this error can occur in the wild. You can freely switch between the two program variants (or even edit the program and click run!); all the diagnostics will update.
As the compiler we need to tell users that the program doesn’t compile. The truly simplest thing we could do is emit
This may look like a joke—I think we can all agree this is unsatisfactory—however, Rust’s trait errors can at times be equivalent to this. This observation was the motivation behind our paper An Interactive Debugger for Rust Trait Errors and the Argus trait debugger. I’ll call this the terse diagnostic variant.
I won’t motivate any more why the above is bad. Let’s add more information to the diagnostic.
MinimalInstead of saying that an error exists, let’s change the text to tell the user which error the typechecker found.
This diagnostic, I argue, is what most compilers emit. It states that a type error was found by the typechecker, prints the expression in which it was encountered, and states the error that occurred: some type was expected, which differed from the actual type of the expression. I call these minimal diagnostics. They contain the bare minimum amount of information that a developer needs to start debugging their program. It’s minimal, instead of, sufficient or great because there are still problems with it.
(move pos) in the distilled example) but this is disjoint from the code.Although the first problem is solved by the Language Server Protocol it’s still a problem for those who don’t use a language server. For example, when working in OCaml, I will open a terminal window and run dune build --watch, which is often faster/easier than using ocaml-lsp. The fix for this problem would be to have a URL or editor-integration to jump to location from the terminal.
The second and third problems are easy to overcome. The compiler performed some typechecking, and it has this information, but we don’t emit it because it would be verbose and for most errors not useful. However, when you do need the information it would be incredibly useful. Developers will often partially simulate typechecking in their head in order to recreate the information. I believe this is also why so many blog posts about Rust ownership start by explaining the borrow-check process: understanding the algorithm helps interpret error messages. We embodied this idea in our Aquascope project, where we generate diagrams that visually explain the borrow checker process for a specific piece of code.
We can fix the second and third problem by emitting more information. However, more is not always better, too much data at once is overwhelming and then diagnostics become hard to read. We’ll talk about how to leverage interactivity later to make more information easier to work with.Hint, let’s borrow some ideas from data visualization.
The fourth problem is tricky because I see it as fundamental to many type checking algorithms. The core issue is that an error message is a diagnostic, not a diagnosis. Here’s how Merriam Webster draws the distinction.
In other words: the typechecker identifies a symptom of the error and it’s up to the developer to determine the cause.
In this simple program there exists a tuple, which is used both as (tuple int int) and (tuple float float); this is a symptom, localized by the typechecker. The actual error depends on what the developer intends for the program to do. If the programmer expects these to be integers, then the issue is with the floating points ops, and vice–versa. This is why the diagnostic should provide as much information as possible so that the developer can easily conclude the root cause of the error.
To try and overcome these 4 problems, we can use some interactivity and ideas from data visualization to change how the information is presented, which brings us to interactive diagnostics.
Most people, when I say “interactive diagnostics,” think that we’re going to provide some dashboard for visualizing type constraints. Although this is not what I’m advocating for here, we can do it quite easily. Let’s take the constraint graph built by the typechecker and render it … as a graph!Using Spytial of course.
Let’s call this the graph diagnostic, which would be a frustrating diagnostic. But it isn’t completely useless. It shows the type variables found while typechecking and all of the subtyping constraints between them. Sure, developers would be pissed if this was the diagnostic, but looking at the graph makes me think of the problem as information flow instead of actual–expected types.
The concrete types int and float have flowed into the same type variable, which can’t be both at the same time. The type mismatch is caused by these flows coming together. Unlike the raw graph, a developer can use these flows as a diagnostic. Diagnosing the problem for the developer is then identifying where a flow should/shouldn’t exist within the code.
With this framing, we can try and revamp the graph diagnostic to show the flows within the constraint graph, rather than just the raw constraint graph itself.Try hovering over the dots for more information!
The flow diagnostic takes the subtyping constraints from the underlying graph, and renders them as arrows between the code variables with those types. The points in the diagnostic show the subtyping rule and a brief reason for why the rules was imposed, e.g., value is pattern matched, used as a function parameter, etc.This very idea is the basis for this paper, but the authors made the mistake of trying to print flows as static text, which made them very verbose.
Instead of making the flows a separate diagnostic artifact, I’ve presented them as an information overlay on top of the actual code. I’m really leaning in to the flow aspect of the information by drawing the arrows on top of the code. If you hover over one of the dots between the arrows, I show the two type variables the information flows between and the reason for flowing (e.g., function paramter, deconstructed value, etc).
The arrows on top of the code do clutter the code. When arrows are close together they can be hard to read. I’ve done some work to make this better, but oftentimes with renderings like this tools will introduce a panel alongside the code. Examples of this style include Aquascope and RustViz. This way the code is still clean and readable. Let’s play the same game here. Instead of drawing the arrows on top of the code let’s introduce a separate panel which contains the same information.
This rendering doesn’t offer any new information; it’s simply the same information rendered differently. But by placing the information in the side panel it becomes harder to see how the type flows from source to sink. Although it’s cleaner, I don’t like it as much. That’s not to say that we couldn’t make it better, this was a first attempt, but I’m not going to fuss around with it any more.
I really enjoy making these visual-based diagnosics because I can get really creative with them. Unfortunately, as programs scale making the visuals gracefully scale is difficult. And if one of these flow diagnostics was the only diagnostic aide developers got, there’d be a revolt. Betting on text-based diagnostics is safe, but it doesn’t need to be static, and it can be more clever than you might think.
TreeFor the final diagnostic, let’s take the flow information and render it as a textual explanation of the problem. One explanation is for Why the expected type was inferred and the second for How was the actual type inferred. This should convey similar information to the flow diagnostics, but we’ll render it as text. Additionally, presenting all of the text at once will be overwhelming. Instead, we’ll provide additional information in dropdowns for when developers need it, but it’ll remain hidden when they don’t want it.
I’ll call this the tree diagnostic: lines alternate as statements and reasons, where a statement may have many reasons. Although the tree diagnostic is not visual, it is still interactive. If you hover over information in the diagnostic, corresponding information in the code also highlights. You could achieve this type of interactivity in the major editors (VS Code, Vim, Emacs) and you could also allow jump to definition, and other niceties, directly in the diagnostic. Of all the diagnostics presented in this post, tree diagnostics are the most plausible as an actual compiler diagnostic.
Here are some properties I like about the tree diagnostic.
The point of the above was not to convince you that one specific type of diagnostic is the best, but to show you how different diagnostics can be, even if they convey more or less the same information. Error diagnostics is more a problem of data visualization than anything and we should think of it as such and experiment with it as such.
I’m delighted that all of the diagnostics in this post are real diagnostic renderings for the Howl language. You can edit the programs in the editors, click run, and the diagnostics will all update. Experimenting will all these styles might sound like a lot of work—it isn’t. Well, not if you structure your compiler the right way. Which brings me to my grander idea of parametric error rendering.
I was inspired to write this post after I sat in on one of Shriram’s programming language lectures. In this lecture Shriram started by talking about high-level differences between a compiler and an interpreter. Using OCaml syntax to describe these functions, we know that an interpreter has the signature:
val interpret : Program -> Value
and a compiler has this signature
val compile : Program -> Program'
Shriram then asked What is the signature for typecheck? The predominant two answers were
Program -> boolProgram -> string optionThe idea being for #2 that the possible string returned is the diagnostic. These answers made me sad. Very sad. Within a few short years of programming these students think that diagnostics are strings and that’s all you need to do. We need to do better to change this mindset.
In my view, typecheck has the signature
val typecheck : Program -> exn option
and to obtain a diagnostic, we need two later functions
type renderer =
| R : { render : exn -> 'a
; view : 'a -> unit }
-> renderer
The render value produces some type 'a, which would be string, or Tui.t, Html.t, or some other medium by which to convey information. The view value consumes that type and shows it to the user. I’ve used an OCaml packed existential so that we can have a list of renderers, which produce and consume different types of information.
This is the exact technique I used to write this blog post. The typechecker for the Howl language throws an exception when it encounters a type error. The exception contains the constraint that failed and the state of the typechecker. All of the diagnostics I wrote are a render and view pair, it’s just that view always produces a React component. It would be trivial to rewrite the view functions to instead produce an interactive TUI panel, a GUI, a VS Code webview panel, a NeoVim/Emacs buffer, etc.
Languages should structure their diagnostics engine this way! It allows us to separate error analysis from error rendering, and allows for developers (like me!) to experiment with alternative ways to analyze, render, and view errors. This type of framework is what made projects like Aquascope and Argus possible, and is the type of framework I’m pushing for in OxCaml.
This also allows us to tailor diagnostics for humans vs. AI agents. It’s still unclear to me how agents should consume type information compared to humans. If it’s easy to extend, modify, change information density, and the format of diagnostics, then we can run more experiments easily and find answers.
As is usual, please email me if you like or dislike what you’ve read.