I don't like naming parameters of functions. Using bruijn indices is a universal reference independent of the function and can actually help readability if you're familiar enough.
This reminds me of the problems that GNU Guix, Nix, and Unison language are trying to solve. The author just seems to be doing it at the deepest layers of the symbolic patterns, rather than relying on hashing.
It really seems like this kind of pattern is a very promising way that would allow us to wrestle back simplicity from the current explosion of complexity.
I imagine a world where every named function is just an alias to a large compendium of well tested, and well understood primitives in a language like this.
I’m glad I came across someone else who’s interested in the idea of having a large compendium of well tested functions.
I’ve been tinkering with an idea where we could compactly map the set of these functions to the set of integers so they’re enumerable in such a way that small integers always correspond with small functions.
A few years ago, I read a paper by Matthew Szudzik about the Rosenberg Strong pairing function and how one could use it to enumerate instances of binary trees such that you will never produce a tree of N+1 level until you’ve exhausted all trees of N.
Relating it to Unison, I always thought encoding to big integers might be an interesting complement their big idea.
Fascinating. I also like the idea of such a compendium.
Wouldn't the binary lambda calculus (BLC) encoding also suffice as a (relatively) compact map to these functions? To convert the encoding to a bigint, you'd just need to prepend a 1 and convert the binary string to decimal as normal.
Honestly, I’ve been meaning to check out BLC encoding some and I really appreciate you posting this. It’s a great read!
I can’t speak to the practical nature of my encoding, but I wanted it to be air tight and to only encode closed terms. For my latest scheme, 0 maps to the identity function and 1 maps to the identity function calling itself.
I just got caught up in the idea of compactly representing all sorts of recursive data types as integers to create an airtight bijection.
That took me down the rabbit hole where I wanted to explore how I could use balanced pairing functions to map to data types instances restricted by constraints. For example, maybe you want to map the integers to the set of terms that can be simply typed, or some other constraint.
The way I see it is if you can come up with ways to declaratively and efficiently select subsets of these bijections, one could reduce some problems to brute force, by shrinking the search space. (Something the Alloy modeling language does)
That’s when I came across this repo and associated paper titled Fair Enumeration Combinators and learned about the SciFe library Scala library.
He has a quote from another article here:
This reminds me of the problems that GNU Guix, Nix, and Unison language are trying to solve. The author just seems to be doing it at the deepest layers of the symbolic patterns, rather than relying on hashing.It really seems like this kind of pattern is a very promising way that would allow us to wrestle back simplicity from the current explosion of complexity.
I imagine a world where every named function is just an alias to a large compendium of well tested, and well understood primitives in a language like this.
Links to the other projects I mentioned:
https://nixos.wiki/wiki/Nix_Hash
https://guix.gnu.org/manual/en/html_node/Features.htmlhttps:...
https://www.unison-lang.org/learn/the-big-idea/