~icefox/determination - Rust versions of TAPL's System F and System F-omega type checkers - sourcehut hg
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.
