What is bidirectional type checking and why would I want to implement it?
It feels like the name is a bit of a misnomer and the syntactic separation kind of resembles stuff like ANF, call by push value or CPS?
Bidirectional type checking is a popular technique for implementing type checking/inference algorithms. AFAIK it originated from the paper "local type inference".
The idea of bidirectional type checking follows from the following observation: there are two ways to typecheck a program, type checking, where type information is provided externally, and the program checks if some term matches the type, and type inference, where type information is missing, and the algorithm must deduce it from only the term itself.
Obviously, inference is much harder than checking. In fact, in many complex type systems only the latter is decidable. However, requiring type annotation everywhere is very awkward. And here comes bidirectional type checking: its ultimate goal is to propagate type information/annotation through the syntactic structure of terms.
There are two modes in bidirectional type checking, synthesis and checking. synthesis corresponds to type inference, and no external information is available. So an annotation is usually needed here. On the other hand, checking mode, as its name indicates, receives a type from the outside world and performs type checking, so usually no type annotation is needed.
At nodes like function application
f(t), where the subterms' types are related, bidirectional type checking can propogate type information from one to the other, reducing the number of annotations needed. For example, if
f synthesis to a type
A -> B, then
t can be checked with
You mentioned CPS/ANF/CBPV. IMO they are not related to local type inference. Local type inference shares with these transformations/NFs the same nature that it reveal certain ordering on terms. However, CPS/ANF reveal evaluation order, while what bidirectional type inference reveals is how type information flows, which is something different.
I think it's referring to a style of implementing type checkers, where you have two mutually recursive functions: one for applying introduction rules and one for applying elimination rules.
The former is usually called
inherit, the latter is usually called