Implementing a functional language with graph reduction (2021)(thma.github.io)

52 pointsby Bogdanp12 miesięcy temu5 comments

thma.github.io

Implementing a functional language with graph reduction (2021)

https://thma.github.io/posts/2021-12-27-Implementing-a-functional-language-with-Graph-Reduction.html

5 comments

tromp12 miesięcy temu

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

taliesinb12 miesięcy temu

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?

ThyerMJ2612 miesięcy temu

The author's previous post goes into details of a categorial connection:

  λ-Calculus, Combinatory Logic and Cartesian Closed Categories
  https://thma.github.io/posts/2021-04-04-Lambda-Calculus-Combinatory-Logic-and-Cartesian-Closed-Categories.html

Also, more in-depth:

  Categorical combinators, P.-L. Curien
  https://www.sciencedirect.com/science/article/pii/S001999588680047X

(or maybe you're looking for something beyond that)

enricozb12 miesięcy temu

Interaction nets are another computational model based on graph-reduction.

https://ezb.io/thoughts/interaction_nets/lambda_calculus/202...

throwaway8152312 miesięcy temu

SPJ's book about the same topic is very good.

https://simon.peytonjones.org/slpj-book-1987/