[EN] Bidirectional Type Checking

When you write a type checker, there are a few ways one might go about it.

First, you can do it outside-in: given an expression and a type, you check that the expression matches that type by inferring the type that the sub expressions should have, then checking that they do. This operation is typically called checking. Here, type information comes from the outside, and it flows into the expression.

For example, let's check that 3+x is an int. First, we realize that both 3 and x need to be int. Now we check that 3 is an int, and discover that it is. Then, we check that x is an int, and if it is, we would be done, and type checking would be successful. If not, then we'd emit a type error.

Second, you can do it inside-out: given an expression, you can infer types for the sub expressions, then use those to infer a type for the full expression. After that, you can check that the inferred type matches what you were expecting. This operation is typically called inference. Here, type information comes from inside the expression, and it flows out.

For example, let's infer a type for 3+x. First, we infer a type for the expression 3, and it turns out to be int. Then, we infer a type for the expression x (we probably just look this up in a symbol table). Then, since we are adding things, they should be of the same type, so we check that the two inferred types are the same. If they're not, we end with a type error, but if they are, we infer that the type of the entire expression is int.

These are fine on their own, but they struggle at different things, like function calls, anonymous functions, sub typing, etc. It turns out that by using checking on some types of expressions and inference on others, we can build more robust type checkers that avoid most of the pitfalls of either one. This idea is called bidirectional type checking.

About me

My name is Sebastian. I'm a competitive programmer (ICPC World Finalist) and coach. I also enjoy learning about programming language theory and computer graphics.

Social links:

Comments

  1. RubabDecember 16, 2022 at 8:00 PM

    Thanks for the great introduction! I have a question. I keep reading that bidirectional typing is good at reporting errors precisely. Could you show an example where it does a better job than any other syntax directed system (e.g., HM) in reporting error?

    ReplyDelete

Post a Comment

Popular posts from this blog

[EN] Writing a Compiler is Surprisingly Easy (part 1)

Part 1: expressions, arithmetic Part 2: statements, control flow Ever since I was a teenager I wanted to create my own systems programming language. Such a programming language would certainly have to be compiled to native code, which meant I'd have to write a compiler. Even though I managed to write several half-working parsers, I'd always fail at the stage of generating assembly code, as the task turned too complex. In this blog I intend to show my teenage self how writing a code generator is, in fact, not complex at all, and it can be fully done in a couple of weekends. (As long as we make some simplifying assumptions) I will that assume you already know that representing programs within a program is surprisingly easy Where do we even start? The goal today is to translate a high level language to x86-64 machine code. Our high-level language will have integer literals, variables, negation, and addition. To make our job simpler, we will translate the hig
Read more

[EN] Representing Programs Within Programs is Surprisingly Easy

Suppose that you want to create a brand new programming language that will change the world. Or that you want to auto-formatter that gets indentation just right . Or maybe you want to write a pre-processor for an existing language, to hack some missing feature into it . Whatever it may be, there are many reasons to write programs that manipulate other programs as data and the first step is to figure out how you are going to represent that data within the program. My goal in this article is to explain one of the most standard approaches (Abstract Syntax Trees) and show how they are actually really easy to understand and implement. This article has many code examples in the C language. What kind of language are we defining? Let's start with a simple example: a language with variables, numbers, and addition. Note that this language does not have statements, but only expressions that evaluate to simple values. This means that we will be able to represent expressions such as
Read more

[EN] Writing a Compiler is Surprisingly Easy (part 2)

Part 1: expressions, arithmetic Part 2: statements, control flow In my first few attempts at writing a compiler, a big hurdle was compiling control flow (conditionals, loops, etc). I think this stemmed from the fact that the a lot of the common advice that's floating around the internet is for writing an optimizing compiler, so I would hear things like 'static single-assignment', 'control flow graphs', 'phi-nodes' and the like, and get lost trying to take it all in. Because of such things, my first serious attempt at implementing a programming language ended up begin a tree-walking interpreter, and it was several years until I dared write a compiler. I'd like to show that all these things, while interesting and valuable in their fields of application, are not required to write a useful compiler. In particular, we'll see at the end that even a naive compilation strategy will handily beat a fast tree-walking interpreter in speed. State
Read more