Conversation
Broken reply chain? Can't see what you're commenting on! 🙂
1
Oh, this one?
Quote Tweet
McBride: Everybody’s Got To Be Somewhere
arxiv.org/pdf/1807.04085
1
Replying to
Yeah, I've seen it before. Looked like it might reduce the performance overhead of a nameless representation... if I could understand it! Might require some more readings/messing around though. I've always struggled with DeBruijn index stuff, and this is at another level… 😂
explained it to me once. As I remember it, the very basic gist of the idea is that where de Bruijn (whether levels or indices) assigns numbers to variables by looking at variable *introductions* (lambdas, if you don't have anything fancier), this looks at *uses*.
1
So where de Bruijn says, "if only one variable has been introduced in this scope, it can only be called 0", this says, "if only one variable is referred to within this scope, it can only be called 0". So at leaves of the tree, at Var nodes, variables are always called 0.
1
1
Show replies