I love this. It looks like this covers a very practical version of a similar buildup that I like [0]. The book I linked is a much shorter textbook path through these type systems than the books linked in the article, and I found it pretty readable.
While that is an excellent book, I would say that it focuses on type theory from a somewhat more theoretical perspective than (say) TAPL which is more on type _systems_ from a programming languages perspective. Both are great reads though.
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.
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?
Slightly out of my depth, but per Diaconescu's theorem [0] axiom of choice implies the law of the excluded middle. Does that make Lean non-constructive?
Yes, but for an even more immediate reason. The axiom of choice itself is a non-constructive axiom. It asserts the existence of the inhabitant of a certain type, without in any way furnishing the inhabitant.
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.
Right, I was about to comment the same thing that "Lean" does not itself assume choice. Mathlib4 does, and Lean4 is designed so that all the built-in stuff is _consistent_ with choice. But you can do purely constructive mathematics in Lean and it's is even designed so that any non-propositions depending on choice have to be annotated "noncomputable", so the walled garden of choice is baked in at a language level. Even within "noncomputable" code, choice still shows up in the axiom list if used.
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.
If I could make a request, I'd love to see resource like this for Linear type systems. I tried reading Henry Baker's Linear Lisp papers, but they were way beyond my skill level.
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)
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.)
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.
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.
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'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.
Related: https://github.com/AndrasKovacs/elaboration-zoo
This is a great resource to learn how normalization by evaluation and insertion and solving of implicit variables is implemented.
I love this. It looks like this covers a very practical version of a similar buildup that I like [0]. The book I linked is a much shorter textbook path through these type systems than the books linked in the article, and I found it pretty readable.
[0] https://anggtwu.net/tmp/nederpelt_geuvers__type_theory_and_f...
While that is an excellent book, I would say that it focuses on type theory from a somewhat more theoretical perspective than (say) TAPL which is more on type _systems_ from a programming languages perspective. Both are great reads though.
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.
There is a great blog post on how the OCaml type checker is inspired by garbage collection here: https://okmij.org/ftp/ML/generalization.html
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.
Slightly out of my depth, but per Diaconescu's theorem [0] axiom of choice implies the law of the excluded middle. Does that make Lean non-constructive?
[0] https://en.wikipedia.org/wiki/Diaconescu%27s_theorem
Yes, but for an even more immediate reason. The axiom of choice itself is a non-constructive axiom. It asserts the existence of the inhabitant of a certain type, without in any way furnishing the inhabitant.
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.
Right, I was about to comment the same thing that "Lean" does not itself assume choice. Mathlib4 does, and Lean4 is designed so that all the built-in stuff is _consistent_ with choice. But you can do purely constructive mathematics in Lean and it's is even designed so that any non-propositions depending on choice have to be annotated "noncomputable", so the walled garden of choice is baked in at a language level. Even within "noncomputable" code, choice still shows up in the axiom list if used.
Yes, in fact Lean proves the law of the excluded middle using Diaconescu's theorem rather than assuming it as an independent axiom:
https://github.com/leanprover/lean4/blob/ad1a017949674a947f0...
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.
If I could make a request, I'd love to see resource like this for Linear type systems. I tried reading Henry Baker's Linear Lisp papers, but they were way beyond my skill level.
Linear(-like) type systems differ from usual functional type systems by their ability to remove bindings from environment.
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
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"
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 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
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!
[flagged]