AFAICS bidirectionality just means "has type inference" [1]. But I'm not sure how useful the term is because just about every language has some small degree of type inference – even in C you don't have to annotate every (sub)expression with its type! Resolving the type of the term `2 + 2` in C is a form of type inference.
C++, C#, and Java have slightly more bidirectionality, as they allow inferring the type of a variable based on its initializer. Function overloading (ad-hoc polymorphism) is also a form of bidirectional type checking.
Rust requires that all function signatures be fully annotated with the exception of lifetimes (mostly for the reasons of clarity and API stability). Function-local type inference is strong, but not fully bidirectional.
[1] https://ncatlab.org/nlab/show/bidirectional+typechecking
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"