Lambda crabs, part 1: A mathematical introduction to lifetimes and regions | Hacker News Reader

Lambda crabs, part 1: A mathematical introduction to lifetimes and regions

ticki.github.io

75 pointsadamnemecek20 comments

These articles explain the mathematical underpinnings of Rust's borrow checker. The explanation is actually fairly simple, but it assumes prior familiarity with abstract algebra.

For people who are unfamiliar with posets, lattices, etc., this introduction might help a bit: http://old.iseclab.org/people/enji/infosys/lattice_tutorial.... (PDF)

For introduction to how Rust's ownership/borrowing/lifetimes system works, see the three chapters starting here: https://doc.rust-lang.org/book/ownership.html

And a "standard disclaimer" for math: To understand this material, you may need to read slowly, look things up, and work through each example. Math is often very simple, but that doesn't mean that it's easy. The trick is usually to stare at it from enough different directions that the underlying simplicity finally "clicks," and you wonder how you could have ever been confused. If you're unfamiliar with the topics in question, a page per day can be a perfectly acceptable reading speed.

Part 2 here: http://ticki.github.io/blog/lambda_crabs_2/

My goodness! A Lattice (not the linear algebra kind, the abstract algebra kind) being used in the wild? I genuinely never thought I'd see those again outside my analysis textbook.

Ticki does really great work in Rust. I think the only thing he's doing that I disagree with is his RFC for a keyword for dynamic dispatch (all we really need is to distinguish trait objects - dynamic dispatch is just the symptom).

Lattices are used to provide a theoretical basis for dataflow analysis in compilers. See Chapter 9 of Aho et al.'s book on compilers.

Ordered sets also occur in denotational semantics http://homepage.cs.uiowa.edu/~slonnegr/plf/Book/Chapter10.pd...

Lattices and the associated Galois connections are used quite a bit in the Abstract Interpretation school of program analysis [1].

[1]: https://en.wikipedia.org/wiki/Abstract_interpretation

Seems to be common among compiler theory people

http://www.cliffc.org/blog/2012/03/24/too-much-theory-part-3...

I know next to nothing about Rust, which makes this all kind of opaque. Can you link a good Getting Started for Rust that pairs well with these?

You can start with this https://doc.rust-lang.org/book/

I think this might be relevant:

https://news.ycombinator.com/item?id=11746913

http://arxiv.org/pdf/1503.07199v1.pdf

How did this make it to the front page? It is so esoteric to begin with, and so poorly explained beyond that... it's not even useful to most of the people it is intended.

All that aside, can we stop making up new words for things that already have words? -- correction, can we stop re-purposing old words for old things and acting like they're new? I mean really, “outlives or equals to”?

> It is so esoteric to begin with

If abstract algebra is so "esoteric" for you, I'm afraid you should rather read Trump speeches instead of following HN.

> I mean really, “outlives or equals to”?

Suggest a better alternative and prove that we should throw away decades worth of papers and start using your new terminology.

FTA: “Regions have an outlive relation defined on them.” Typo? Should that be outlives?

We say equality, inequality, equivalence (equal valence, i.e. value) relation. To be equal -> equality. To outlive -> ? Valid question, outlives doesn't quite fit? To exceed the lifetime, to go beyond the region -> an excession relation, an overboundedness relation? I jest (in part). Naming things is hard! One of the two hard things in programming, as they say.

> Suggest a better alternative and prove that we should throw away decades worth of papers and start using your new terminology.

“outlives or equals to” -> “outlives or is equal to in scope/duration” reads better to my ears.

So it's not even to outlive, it's to live for the same amount as or outlive.

GP has valid language use concerns. And yes, abstract algebra is esoteric.

ps: The Trump swipe is crass.

Outlive -> Outlivity? :-)

I think talking about the "outlives" relation is reasonably clear. "A outlives B (written B < A) if ...".

The relation for <= could be written "outlives or is equal to", or "lives at least as long as". Thus "B <= A" could be spoken "A lives at least as long as B", or "A outlives or is equal to B".

Ok, I see, 'outlives' is much better. But I guess he's complaining about the very choice of the relationship names, not nitpicking about grammar.

> abstract algebra is esoteric.

How is it so? It's fundamental and essential. "Esoteric" implies "mostly useless", which is definitely not true.

Cool. No way am I saying that abstract algebra is mostly useless, not at all. There's another sense for `esoteric'[2] which means hidden (or secret?) or highly specialised[0] or rare or unconventional. Which I think is what is being got at here, a sort of math-cult[1] if you will :)

[0] http://www.thefreedictionary.com/esoterica

[1] https://en.wikipedia.org/wiki/Western_esotericism

[2] http://www.thefreedictionary.com/esoteric

edit: I agree, abstract algebra is fundamental, beautiful, and essential - but in fairness, it is highly domain specific and if Rust's type system can be explained as exactly and succinctly with terms closer to home thenwe ought to give it a shot

> it is highly domain specific

It is "domain specific" to pretty much all the domains in existence.

Word choices aside, my original question is a legitimate one. How does something like this gain rank? B/c there's no way a majority of Hacker News readers saw this, read it, and thought "great article -- up vote!"

I'm among the upvoters. I have been hearing a lot about Rust, and its unique feature is its memory management, but the official Rust documentation is not as clear as it could be. I was building up courage to go read the compiler sources, so I found the article very timely and useful.

For what it's worth, we also know that, and I'm in the process of re-doing it. The official docs will never present it like this, though, as they're more targeted towards working programmers than type theory experts, and so I'm excited to see more articles like this pop up.

I guess for a majority of HN readers abstract algebra is not "esoteric", and type systems is a very hot topic indeed.

Even those pitiful articles from the dynamic typing zealots are very often coming to the front page, so a high quality explanation of a trendy topic in the modern type systems research should definitely attract a lot of attention.

Reply on news.ycombinator.com