Hm that page says bidirectional type checking is a style of mathematical presentation of a type theory AND a kind of algorithm for implementing one
and that it splits the judgement ... into two parts, for checking and synthesis/inference
That doesn't seem equivalent to "has type inference".
I quoted Chris Lattner below, and I think he MAY have been using "bidirectional" in that sense, to explain why the Swift type checker is slow.
But that just reinforces my opinion that people are using the term "bidirectional type checking" in different ways.
---
Where are the typing judgements for Go, Zig, Rust, Swift? I don't think they exist, because those languages seem to be defined more by algorithms than sets / judgements.
If that's true, then according to the definition you quoted, they DON'T use bidirectional type checking.
But all of them have limited forms of type inference.
Also my reading now is that "bidirectional" actually is in contrast to Hindley-Milner, which is unidirectional in the synthesis / inference direction
There is the THIRD choice of Go / Zig / Java, which are unidirectional but CHECKING-oriented - the opposite of Hindley-Milner
---
That is, I don't think it makes sense to define Go as "bidirectional" because it does a little inference around the LHS and RHS.
This seems to be another case where two different camps use the same word in different ways
(which is not surprising if you observe that a similar confusion happens with the word "type" itself - https://kar.kent.ac.uk/69703/ )
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
has type inference, but doesn't require mutual recursion of checking and synthesisi.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"