CHchubot·Aug 18, 2025
This seems to jump straight into type inference and bidirectional type checking, without a basic UNI-directional type checker
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. G
Read the rest
o, 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.