https://github.com/leanprover/lean4/blob/ad1a017949674a947f0...
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.
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.
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
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
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.
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/ )
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))
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
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.)
[0] https://anggtwu.net/tmp/nederpelt_geuvers__type_theory_and_f...
voidUpdate•5mo ago
webstrand•5mo ago
MarkusQ•5mo ago
darth_aardvark•5mo ago