On: Typechecker Zoo

According to that source, one direction is checking if a fully annotated program is well-typed (as in, prove equations with no unknowns) and the other direction is inferring types in a program where not everything is typed (the equations contain unknowns, which must be computed and checked that there’s exactly one solution).

I think this is false: bidirectionality just means "has type inference"

Swift, Rust, Go, and Java all have some kind of type inference

Swift and Rust appear to use bidirectional type checking, but Go and Java don't

The issue seems to be that say

    a := f(x, g(y))

has type inference, but doesn't require mutual recursion of checking and synthesis

i.e. type inference is a feature of a langauge; bidirecitonal type checking is an algorithm that may or may not be used to implement it

I have occasionally seen people make the distinction by talking about type deduction vs type inference.

Yeah that may be a good distinction -- I see that C++ auto is often called "type deduction"