[0] https://anggtwu.net/tmp/nederpelt_geuvers__type_theory_and_f...
But Lean sequesters off the classical logic stuff from the default environment. You have to explicitly bring in the non-constructive tools in order to access all this. So, actually, I would disagree with GP that Lean's type system includes a choice axiom.
https://github.com/leanprover/lean4/blob/ad1a017949674a947f0...
e.g. Featherweight Java (chapter 19 of TAPL by Pierce) is expressed with a simple unidirectional algorithm
And some of the languages in the PL Zoo - https://plzoo.andrej.com/
like https://github.com/andrejbauer/plzoo/blob/master/src/sub/typ... , although I am not quite sure
related thread: https://old.reddit.com/r/ProgrammingLanguages/comments/sq3z3...
---
I also think these statements are suspect:
We’re going to create minimal implementations of the most successful static type systems of the last 50 years.
As a result, many modern statically-typed languages have converged on a practical and elegant middle ground: bidirectional type checking.
I think what is missing in both statements is the word FUNCTIONAL.
e.g. Go, Rust, Swift, D, and Zig are modern statically typed languages, that are not functional. And I'm not sure if the authors would consider them "bidirectional"
I would like to see someone write about that. (I posed this query to 3 LLMs, and they mostly agree that those languages don't use bidirectional type checking; however I am wary of repeating AI slop)
e.g. this is a very good survey along those lines: https://thume.ca/2019/07/14/a-tour-of-metaprogramming-models...
---
This part also reminds me of Against Curry-Howard Mysticism - https://liamoc.net/forest/loc-000S/index.xml - https://lobste.rs/s/n0whur/against_curry_howard_mysticism
A deep insight has been unfolding since the late 1970s, a revelation that three immense, seemingly distinct realms of human thought are echoes of a single, deeper reality.
However, both languages have significant limitations on bidirectionality, mainly due to their embrace of dot syntax. If you write `foo.bar`, the compiler can't look up `bar` without first knowing the type of `foo`. So types cannot fully propagate backwards through such expressions (i.e. if the compiler knows the type of `foo.bar`, it cannot infer the type of `foo`).
There is an exception if the type is partially known: if the compiler knows that `foo` is of type `Vec<_>` (without knowing the type parameter), and also knows that `foo.pop().unwrap()` is of type `i32`, it can conclude that the type parameter is `i32`. But it couldn't do this if `foo`'s type were completely unknown.
This contrasts with more-traditional functional languages like Haskell and OCaml, where (to slightly oversimplify) there is no dependent name lookup. Instead of `foo.bar()`, you would write `bar foo`. This means the compiler doesn't need to know the type of `foo` to look up `bar`, improving bidirectionality. But in exchange you can only have one `bar` in scope at a time. (`bar` can potentially be a generic/typeclass function that works differently for different types, but you can't just have unrelated methods on different types that happen to have the same name. Or rather, you can, but if you do then you have to manually choose which one you want in scope.)
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
This comment says Rust's type inference is not Hindley-Milner, but rather it's "influenced by" bidirectional type checking: https://lobste.rs/s/hbzctm/type_inference_rust_c
(but I think that is about type inference; I think there are parts of the Rust's type checking algorithm that could be described with different terms)
---
This post quotes Chris Lattner on Swift, saying
https://danielchasehooper.com/posts/why-swift-is-slow/
My experience with Swift is we tried to make a really fancy bi-directional Hindley-Milner type checker
So I guess this hints at what I suspected -- that people mean different things when they say "bidirectional"
---
But also, it's probably reasonable to put Go and Zig (?) in one category, and Swift and Rust in another