Typechecker Zoo

https://sdiehl.github.io/typechecker-zoo/

by todsacerdoti • 11 months ago

193 31 11 months ago

sdiehl.github.io

voidUpdate• 11 months 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• 11 months 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• 11 months ago

In that case, why so big?

darth_aardvark• 11 months ago

He's got a lambda eyebrow!

etiamz• 11 months ago

dunham• 11 months ago

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

tromp• 11 months 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?

cwzwarich2• 11 months ago

Lean’s type theory extends CIC with the (global) axiom of choice, which increases consistency strength over base CIC.

wk_end• 11 months 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

_verandaguy• 11 months 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.

chubot7• 11 months 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/

like https://github.com/andrejbauer/plzoo/blob/master/src/sub/typ... , although I am not quite sure

---

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.

Ar-Curunir• 11 months ago

Rust uses bidirectional type checking

chubot7• 11 months ago

What makes you say that? What's your definition of bidirectional type checking?

comex• 11 months ago

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

choeger• 11 months 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• 11 months 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

6gvONxR4sf7o• 11 months 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_f...

shadowfox• 11 months 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• 11 months 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• 11 months ago

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

Typechecker Zoo

Related Stories