This is a great resource to learn how normalization by evaluation and insertion and solving of implicit variables is implemented.
To the author: consider adding a dark theme to the code blocks. As-is, viewed on a system with a dark theme, these default to a really low-contrast light theme that's hard to read even without vision issues.
The CoC implementation includes inductive types, so is this an implementation of CiC, the Calculus of Inductive Constructions, with the same proving power as Lean?
Lean’s type theory extends CIC with the (global) axiom of choice, which increases consistency strength over base CIC.
Proposal: Also implement the efficient Hindley/Milner variant used by the OCaml compiler. IIRC it is inspired by garbage collection and much faster than the original.
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. 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.
Rust uses bidirectional type checking
As does Swift.
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.)
What makes you say that? What's your definition of bidirectional type checking?
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
Well I Googled myself since I was curious
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 type inference; I think there are parts of the Rust's type checker 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
I'm a little confused by the cutesy animal pictures on the first page... The only one that doesnt have some kind of lambda scribbled on them is the one that is directly lambda calculus, and I can't work out what some of the other symbols are even meant to be...
I'm pretty sure they're AI generated art, I don't think the symbols are intentional or have any meaning. They're basically ornamental section dividers.
In that case, why so big?
He's got a lambda eyebrow!
Unecessary AI generated slop no one asked for, that made me close the webpage. When will authors realize that unrelated ugly AI art only removes values from their articles?