An attempt at making type checkers for System F and System Fω. Based largely off of Pierce's Types And Programming Languages reference implementations, available here. I ported them from OCaml to Rust, mainly 'cause I find that a good way to go through all the details of a program and understand how they work. I've included copies of the relevant ones for easier reference and to help with debugging.

There's a few differences, but mostly superficial ones. The original TAPL languages include a parser and interpreter. I'm only interested in the type checker, so my ports just take an AST and does the type checking. The originals use pure de Bruijn indices for the variables and include a check digit of the expected environment length, but only the interpreter actually checks it, so I take it out and replace it with a variable name for debugging. I also clean up loooooots of the variable names and nonsense like that; some of it is due to Rust having nicer type namespacing than OCaml, some of it is due to the TAPL version being basically uncommented and horribly named. Turns out that if you want to understand the TAPL code, the way you do it is by reading it alongside the book chapters that discuss it. I wonder if that was intended to be a bit of copy protection, or whether it just ended up that way as academic code written alongside a book?

Also note that the TAPL type checkers include no type inference, while in 2024 at least some amount of type inference is so common its lack is worth pointing out. So if you come here expecting HM or unification or such you'll be disappointed.

TAPL versions of the type checkers are built with make. My versions are built with cargo build.

System F type checkers:

• fullpoly: TAPL version of the typechecker+interpreter
• sys-f: My port of the same thing, with only the type checker

System Fω type checkers:

• fullomega: TAPL version
• sys-fomega: My port of fullomega (only typechecker)
• sys-fomega-nicer: My version with some (more) refactoring and code cleanup, and variable/function names that don't drive me bonkers. The original version is still useful so you can compare 1-to-1(ish) with the OCaml fullomega impl, but there's a lot of small places where it is, with love, slightly academic-quality code. None of that really changes its actual functioning, but it sure gets on my nerves.
• sys-fomega-nbe: An attempt at taking sys-fomega-nicer and replacing all the the de Bruijn index shifting with normalization-by-evaluation, to see if it makes anything easier. It... mostly does? Kinda the magnum opus of this project, since it is a pretty significant revamp and it actually works.

Some other stray bits and pieces:

• lc-nbe: an (untyped) lambda calculus interpreter using normalization-by-evaluation, transliterated from an OCaml version by Brendan Zab in an attempt to understand NbE.

If I get around to it, implement the F-ing Modules and 1ML papers so I understand how they work, 'cause they compile to Fω.

#Related resources:

• brendanzab's Language Garden, a bunch of interpreters and elaborators and such implemented in different styles, letting one compare and contrast the mechanical differences between them.
• Some of UTexas's lecture notes for CS345, one of the best explainations of System F I've encountered so far.
• A github repo with TAPL's code examples here, cleaned up for a more modern OCaml toolchain. I neither need or want that, but I could see it being useful.

#License

idk MIT or something. I don't own the TAPL implementations.