In Haskell, there's the excellent paper Typing Haskell in Haskell which acts as a tutorial on how the Hindley Milner type checker that powers the Haskell compilers work. In the past I've used this to write a Hindley Milner type checker on a lambda calculus, as an exercise to understand the internal algorithms of Haskell type checking.
I'd like to do the equivalent thing for Rust: implement a borrow checker for a simple language (say, a variant of a simply typed lambda calculus). Are there any resources that describe the borrow checker's typing rules in an accessible way, to help me get started on this? Ideal would be a tutorial like the Typing Haskell in Haskell paper linked above, but something like a paper or blog post describing the typing rules would also be useful.
I think the description in the NLL RFC is probably the best one available that's both detailed enough to actually write an implementation, yet still comprehensible for a sufficiently motivated person that's not already an expert on borrow checkers.
I'm not personally aware of any similar writeup for today's "AST borrow check" algorithm.
Hi, does anyone know of anything like this that's more recent? I'm basically just bumping this thread because I have the same question, and I'm really looking for more. Thanks for any pointers.
I don't know the internal details of how it is implemented in Rust, but AST is not enough for borrow checker. Building a CFG after AST will be one way of doing it: Control-flow graph - Wikipedia