[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 infer...