In 2000, Pierce and Turner introduced a new technique to perform type inference for ML-like languages, whose main idea was to carefully understand the local flow of information in typing rules. This technique, which came to be referred to as bidirectional typing, did not come out of a void: similar ideas had appeared independently in other contexts. In particular, bidirectional typing has been a part of the folklore of dependently typed languages implementers since the dawn of time.

But even in that context where it has a long history, bidirectional typing was missing an understanding that would detach from implementations to focus on the type-theoretic structure. Fortunately, such a type-theoretic bidirectional structure turns out to be a very interesting tool when studying (dependent) type systems.

In my talk, I will try and give some of my understanding of bidirectional typing, how it is both rooted in type-checker implementations but is more than just this, and how it can be used to make the infamously painful meta-theory of dependent type systems a bit less painful.