Metaprogramming and self-interpretation of lambda calculus
text.marvinborner.de
text.marvinborner.de
He has a quote from another article here:
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.
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:...
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.
https://gist.github.com/sgoguen/46200419194eb29b82079b0804e5...
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.
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.
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.
https://github.com/ikuraj/SciFe
But practically speaking, I suspect you’re right about BLC being a good practical candidate for an index.
Again, great post!