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?
$\begingroup$
$\endgroup$
6
asked Mar 18, 2022 at 23:41
-
9$\begingroup$ Just wanted to plug the paper Bidirectional Typing by Jana Dunfield and Neel Krishnaswami. It's a fantastic overview of the history, motivation, and implementation of bidirectional type checking. $\endgroup$– Matthew McQuaidCommented Mar 19, 2022 at 1:55
-
$\begingroup$ @MatthewMcQuaid thanks. Part 8.1 also goes into the heriditary substitution, beta normal eta long stuff that I didn't understand the relationship to bidirectional typing about. Part 6.5 is also helpful to me. I was basing my system on linear logic and got confused about symmetries. $\endgroup$– Ms. Molly Stewart-GallusCommented Mar 19, 2022 at 4:06
-
$\begingroup$ Of interest: Theorem Proving in Lean Building Theories and Proofs Pay attention to the word elaborator. I also saw elaborator used with this Idris paper Elaborator Reflection: Extending Idris in Idris. Still trying to move the puzzle piece elaborator into place for the big picture but now that it is on my radar will be more attentive to taking not of it when reading. $\endgroup$– Guy CoderCommented Mar 19, 2022 at 10:34
-
5$\begingroup$ I also want to mention McBride, who is a fervent champion of bidirectional ideas. He has a nice blog post on the subject here pigworker.wordpress.com/2018/08/06/basics-of-bidirectionalism, and a paper I wish very hard he would publish one day there github.com/pigworker/TypesWhoSayNi, both very interesting on the subject. $\endgroup$– Meven Lennon-Bertrand ♦Commented Mar 19, 2022 at 21:14
-
1$\begingroup$ I find this to be a very clear introduction davidchristiansen.dk/tutorials/bidirectional.pdf $\endgroup$– user833970Commented Apr 8, 2022 at 20:10
|
Show 1 more comment
2 Answers
$\begingroup$
$\endgroup$
6
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 A.
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.
-
$\begingroup$ Thanks for this answer! This is better than mine $\endgroup$– ice1000 ♦Commented Mar 19, 2022 at 3:03
-
$\begingroup$ Nice explanation! Let me mention "An algorithm for type-checking dependent types" by Thierry Coquand (pdf) which predates Pierce and Turner, though I think it is correct to credit PT98 with popularizing the concept. One fun thing about Coquand's paper is that there is an appendix with a full code listing of the algorithm! $\endgroup$ Commented Mar 19, 2022 at 17:21
-
2$\begingroup$ It’s even older than this! The first ever implementation of the Calculus of Constructions by Huet as described in
The Constructive Enginehas essentially the same structure as that of Coquand. Actually, I do not think anyone has ever implemented a non-bidirectional typing algorithm for dependent types. $\endgroup$ Commented Mar 19, 2022 at 21:10 -
$\begingroup$ @MevenLennon-Bertrand Isn't Coq's basic type-checking largely inference-based? For example, it's quite common to annotate λ-bound variables and Σ-introductions with types so as to allow for type inference on them, as opposed to in standard bidirectional systems where both would be checked. $\endgroup$ Commented Mar 21, 2022 at 21:45
-
$\begingroup$ Indeed, Coq is designed so that any term infers a type in the kernel. But a lot of Coq is in the elaboration layer, where this is definitely not true, and bidirectional ideas really appear. Then the structure of the kernel is very close to that of elaboration, with fancy features (unification, typeclasses/canonical instances, and so on) removed, but it is still in some way bidirectional. If you look at the proven-correct kernel of MetaCoq, there’s definitely non-trivial bidirectional stuff going on there! $\endgroup$ Commented Mar 22, 2022 at 9:51
$\begingroup$
$\endgroup$
1
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 check or inherit, the latter is usually called infer or synthesize.
-
1$\begingroup$ "one for applying introduction rules and one for applying elimination rules" -- it turned out that in practice people occasionally do use both checking and synthesis for the same introduction rules. So the general guideline does separate on inference-elimination, but in certain cases one can cross it both ways. :) $\endgroup$ Commented Apr 7, 2022 at 8:40