5 ms·

Typechecker Zoo

193 points by todsacerdoti 1y ago

voidUpdate 1y ago
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...
- webstrand 1y ago
  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.
  - MarkusQ 1y ago
    In that case, why so big?
- thrance 1y ago
  [flagged]
- darth_aardvark 1y ago
  He's got a lambda eyebrow!
etiamz 1y ago
Related: https://github.com/AndrasKovacs/elaboration-zoo https://github.com/AndrasKovacs/elaboration-zoo
- dunham 1y ago
  This is a great resource to learn how normalization by evaluation and insertion and solving of implicit variables is implemented.
tromp 1y ago
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?
- cwzwarich 1y ago
  Lean’s type theory extends CIC with the (global) axiom of choice, which increases consistency strength over base CIC.
  - wk_end 1y ago
    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 https://en.wikipedia.org/wiki/Diaconescu%27s_theorem
    - cwzwarich 1y ago
      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/ad1a017949674a947f0d6794cbf7130d642c6530/src/Init/Classical.lean#L35-L67 https://github.com/leanprover/lean4/blob/ad1a017949674a947f0...
    - cvoss 1y ago
      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.
      - nrds 1y ago
        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.
_verandaguy 1y ago
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.
chubot 1y ago
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/ https://plzoo.andrej.com/ like https://github.com/andrejbauer/plzoo/blob/master/src/sub/type_check.ml 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/sq3z3u/good_textbook_with_implementations_of_oo_type/ 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-for-generics/ 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://liamoc.net/forest/loc-000S/index.xml - https://lobste.rs/s/n0whur/against_curry_howard_mysticism 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.
- Ar-Curunir 1y ago
  Rust uses bidirectional type checking
  - chubot 1y ago
    What makes you say that? What's your definition of bidirectional type checking?
choeger 1y ago
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.
- hnra 1y ago
  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 https://okmij.org/ftp/ML/generalization.html
deleted 1y ago
[deleted]
6gvONxR4sf7o 1y ago
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_formal_proof_an_introduction.pdf https://anggtwu.net/tmp/nederpelt_geuvers__type_theory_and_f...
- shadowfox 1y ago
  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.
HexDecOctBin 1y ago
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.
- thesz 1y ago
  Linear(-like) type systems differ from usual functional type systems by their ability to remove bindings from environment.

193 points by todsacerdoti 1y ago

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...

webstrand 1y ago
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.
- MarkusQ 1y ago
  In that case, why so big?
thrance 1y ago
[flagged]
darth_aardvark 1y ago
He's got a lambda eyebrow!

etiamz 1y ago

Related: https://github.com/AndrasKovacs/elaboration-zoo https://github.com/AndrasKovacs/elaboration-zoo

dunham 1y ago
This is a great resource to learn how normalization by evaluation and insertion and solving of implicit variables is implemented.

tromp 1y ago

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?

cwzwarich 1y ago
Lean’s type theory extends CIC with the (global) axiom of choice, which increases consistency strength over base CIC.
- wk_end 1y ago
  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 https://en.wikipedia.org/wiki/Diaconescu%27s_theorem
  - cwzwarich 1y ago
    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/ad1a017949674a947f0d6794cbf7130d642c6530/src/Init/Classical.lean#L35-L67 https://github.com/leanprover/lean4/blob/ad1a017949674a947f0...
  - cvoss 1y ago
    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.
    - nrds 1y ago
      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.

_verandaguy 1y ago

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.

chubot 1y ago

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/ https://plzoo.andrej.com/ like https://github.com/andrejbauer/plzoo/blob/master/src/sub/type_check.ml 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/sq3z3u/good_textbook_with_implementations_of_oo_type/ 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-for-generics/ 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://liamoc.net/forest/loc-000S/index.xml - https://lobste.rs/s/n0whur/against_curry_howard_mysticism 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.

Ar-Curunir 1y ago
Rust uses bidirectional type checking
- chubot 1y ago
  What makes you say that? What's your definition of bidirectional type checking?

choeger 1y ago

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.

hnra 1y ago
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 https://okmij.org/ftp/ML/generalization.html

deleted 1y ago

[deleted]

6gvONxR4sf7o 1y ago

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_formal_proof_an_introduction.pdf https://anggtwu.net/tmp/nederpelt_geuvers__type_theory_and_f...

shadowfox 1y ago
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.

HexDecOctBin 1y ago

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.

thesz 1y ago
Linear(-like) type systems differ from usual functional type systems by their ability to remove bindings from environment.