I think he's using the term "bi-directional" in a potentially confusing and nonstandard way. As I understand it, in this area, that term typically describes a s

I think he's using the term "bi-directional" in a potentially confusing and nonstandard way. As I understand it, in this area, that term typically describes a style of type checking and inference which arose later, and which involves both checking rules and synthesizing rules (the two directions), and which can be made to support some quite expressive type systems, but generally requires programs to have a sprinkling of explicit annotations. On that topic, I found these notes to be very helpful: https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bidirectional.pdf https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bid... But as I understand it, the concept started here: http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf