A similar implementation of a large subset of Haskell was done by Ben Lynn in a winning IOCCC entry as described at [1]. The graph reduction engine is the small C programs shown in [2].
A much larger and more production-ready implementation of Haskell into combinatory logic was made by Lennart Augustsson [3].
Given that whole name binding thing is ultimately a story of how to describe a graph using a tree, I was primed to look for monoidal category-ish things, and sure enough the S and K combinators look very much like copy and delete operators; counit and comultiplication for a comonoid. That’s very vibe-based, anyone know of a formal version of this observation?
A similar implementation of a large subset of Haskell was done by Ben Lynn in a winning IOCCC entry as described at [1]. The graph reduction engine is the small C programs shown in [2].
A much larger and more production-ready implementation of Haskell into combinatory logic was made by Lennart Augustsson [3].
[1] https://crypto.stanford.edu/~blynn/compiler/
[2] https://crypto.stanford.edu/~blynn/compiler/c.html
[3] https://github.com/augustss/MicroHs
Given that whole name binding thing is ultimately a story of how to describe a graph using a tree, I was primed to look for monoidal category-ish things, and sure enough the S and K combinators look very much like copy and delete operators; counit and comultiplication for a comonoid. That’s very vibe-based, anyone know of a formal version of this observation?
The author's previous post goes into details of a categorial connection:
Also, more in-depth: (or maybe you're looking for something beyond that)Interaction nets are another computational model based on graph-reduction.
https://ezb.io/thoughts/interaction_nets/lambda_calculus/202...
SPJ's book about the same topic is very good.
https://simon.peytonjones.org/slpj-book-1987/