Tutorial on implementing a borrow checker on a simplified language?


#1

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.


#2

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.


#3

Excellent, thank you!


#4

There’s also this series of posts by Ticki:

http://ticki.github.io/blog/lambda-crabs-part-1-a-mathematical-introduction-to-lifetimes-and-regions/

At some point hey had “here’s a borrow checker in 400 lines of code” but I can’t find it…