3 ms·

The Faust compiler uses de Bruijn indices internally to reuse computations. Anyone else know any other examples? https://github.com/grame-cncm/faust https://gi

• dunham 1y ago
  Idris[1] and most of the dependent typed languages that I've looked at use de Bruijn numbers. (As does my own[2].) The Idris implementation also has a list of names in scope as an argument to the type of a Term, which makes the compiler (also Idris) check if you're making a mistake with your de Bruijn indices. (I did not do this in mine, but I should have.) Edit: Oh, I see you mention reusing computations, that may be a bit more subtle. I'll have to look at your repo to see what you mean by that. [1]: https://github.com/idris-lang/Idris2 https://github.com/idris-lang/Idris2 [2]: https://github.com/dunhamsteve/newt https://github.com/dunhamsteve/newt
  • matheist 1y ago
    Thanks! (Just clarifying, it's not my project)