Semantic Domain: Bidirectional Typechecking That Does Not Stop
Wednesday, May 13, 2026
Bidirectional Typechecking That Does Not Stop
I’ve been implementing a new language, and one of the things I have<br>been doing is implementing a language server for the first time.<br>Interestingly, this has changed how I will write bidirectional<br>typecheckers from now on!
A bidirectional type system is a set of (syntax-directed) rules with<br>a mode assignment, telling you which bits of the rules are inputs, and<br>which bits are outputs. This lets you transcribe the rules more or less<br>directly to a functional program, which halts with an error when the<br>rule that is supposed to apply, doesn’t.
For example, here are some rules for the simply-typed lambda calculus<br>with booleans, functions, and n-ary tuples:
\[<br>\newcommand{\Rule}[2]{\frac{\displaystyle #1}{\displaystyle #2}}<br>\newcommand{\judgsyn}[3]{{#1} \vdash {#2} \Rightarrow {#3}}<br>\newcommand{\judgchk}[3]{{#1} \vdash {#2} \Leftarrow {#3}}<br>\newcommand{\bnfalt}{\;\;|\;\;}<br>\newcommand{\ms}[1]{\mathsf{#1}}<br>\newcommand{\True}{\ms{true}}<br>\newcommand{\False}{\ms{false}}<br>\newcommand{\ifte}[3]{\ms{if}\;{#1}\;\ms{then}\;{#2}\;\ms{else}\;{#3}}<br>\newcommand{\fun}[1]{\lambda {#1}.\,}<br>\newcommand{\tuple}[2]{\left\langle {#1}_{0}, ..., {#1}_{#2}<br>\right\rangle}<br>\newcommand{\letv}[2]{\ms{let}\;{#1} = {#2}\;\ms{in}\;}<br>\newcommand{\lettuple}[4]{\letv{\tuple{#1}{#2}}{#3}{#4}}<br>\]
\[<br>\begin{array}{cc}<br>\Rule{ \ms{b} \in \{\True, \False\} }<br>{ \judgchk{\Gamma}{\ms{b}}{2} }<br>\Rule{ \judgsyn{\Gamma}{e_1}{2} \qquad<br>\judgchk{\Gamma}{e_2}{A} \qquad<br>\judgchk{\Gamma}{e_3}{A} }<br>{ \judgchk{\Gamma}{\ifte{e_1}{e_2}{e_3}}{A} }<br>\\[1em]<br>\Rule{ \judgchk{\Gamma, x:A}{e}{B} }<br>{ \judgchk{\Gamma}{\fun{x}{e}}{A \to B} }<br>\Rule{ \judgsyn{\Gamma}{e_1}{A \to B} \qquad<br>\judgchk{\Gamma}{e_2}{A} }<br>{ \judgsyn{\Gamma}{e_1\,e_2}{B} }<br>\\[1em]<br>\Rule{ \forall i \in [n]. \judgchk{\Gamma}{e_i}{A_i} }<br>{ \judgchk{\Gamma}{\tuple{e}{n}}{A_1 \times \ldots \times A_n} }<br>\Rule{ \judgsyn{\Gamma}{e_1}{A_1 \times \ldots \times A_n} \qquad<br>\judgchk{\Gamma, x_1:A_1, \ldots, x_n:A_n}{e_2}{C}<br>{ \judgchk{\Gamma}{\lettuple{x}{n}{e_1}{e_2}}{C} }<br>\\[1em]<br>\Rule{ x:A \in \Gamma }<br>{ \judgsyn{\Gamma}{x}{A} }<br>\Rule{ \judgsyn{\Gamma}{e_1}{A} \qquad<br>\judgchk{\Gamma, x:A}{e_2}{C}<br>{ \judgchk{\Gamma}{\letv{x}{e_1}{e_2}}{C} }<br>\\[1em]<br>\Rule{ \judgsyn{\Gamma}{e}{A} \qquad A = C }<br>{ \judgchk{\Gamma}{e}{C} }<br>\Rule{ \judgchk{\Gamma}{e}{A} }<br>{ \judgsyn{\Gamma}{(e:A)}{A} }<br>\end{array}<br>\]
Here’s some Ocaml that takes an expression language like this, and<br>then typechecks it, annotating every subexpression with its type. You<br>can think of it as an implementation of Conor<br>McBride’s subject mode in her approach to bidirectional<br>typechecking.
She explains the subject mode as you start out with a<br>possibly-incorrect program, but if typechecking succeeds, then you have<br>learned that it is actually a well-typed program. I tend to think of<br>modes as just input and output (albeit possibly interleaved), and I<br>think of her subject mode as the simplest form of elaboration: you input<br>an untyped term, and the algorithm outputs a typed term identical in<br>shape.
To do this, obviously we’re going to need a type of types and<br>expressions, with the expressions having the ability to carry some extra<br>information on each subterm. This is easy to do with a mutually<br>recursive datatype, where we have the constructors, and a node<br>constructor that takes a pair of some info plus a constructor:
type tp = Bool | Arrow of tp * tp | Tuple of tp list
module Exp = struct<br>type var = string
type 'info exp' =<br>| BLit of bool<br>| If of 'info t * 'info t * 'info t<br>| Lam of var * 'info t<br>| App of 'info t * 'info t<br>| Annot of 'info t * tp<br>| Var of var<br>| Let of var * 'info t * 'info t<br>| Tuple of 'info t list<br>| LetTuple of var list * 'info t * 'info t
and 'info t = In of ('info * 'info exp')
We will also need some auxilliary functions to get the shape and<br>info, and to build terms without too many parentheses.
let shape (In(info, e')) = e'<br>let info (In(info, e')) = info<br>let make info e' = In(info, e')<br>let update f e = make (f (info e)) (shape e)
module Mk = struct<br>let blit info b = make info (BLit b)<br>let if' info e1 e2 e3 = make info (If(e1, e2, e3))<br>let lam info x e = make info (Lam(x, e))<br>let app info e1 e2 = make info (App(e1, e2))<br>let annot info e tp = make info (Annot(e, tp))<br>let var info x = make info (Var x)<br>let let' info x e1 e2 = make info (Let(x, e1, e2))<br>let tuple info es = make info (Tuple es)<br>let lettuple info xs e1 e2 = make info (LetTuple(xs, e1, e2))<br>end<br>end
Then, we can turn the rules above into a mutually recursive function,<br>which analyses the shape of the term and applies the appropriate rule to<br>it. But before we do that, we’re going to take on board a useful idea of<br>Conor’s: the idea of a pattern.
In the inference rules above, many of the rules look at the shape of<br>a type – is it an boolean, a tuple, an arrow? They all say things like<br>\(A \to B\), where we look at the<br>outermost level, and if...