Tutorial on implementing a borrow checker on a simplified language?

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.

3 Likes

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 Likes

Excellent, thank you!

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…

1 Like

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: https://en.wikipedia.org/wiki/Control-flow_graph