|
|
|
|
|
|
by kmill
1536 days ago
|
|
|
I've messed around with this same graphical language, though only on paper. As I understand it, the lambda/apply nodes are the two morphisms for reflexive objects[1], and these are something like string diagrams for them -- though I haven't fully understood how to interpret oriented wires from this point of view... There a paper referenced by [2] (a project shared on HN in the last couple months) that goes into a graphical language for lambda calculus with the same apply/lambda nodes, but with explicit copying and dropping. The paper is Lafont, "Interaction Combinators" from 1997. (You have to squint to see why it's got anything to do with the lambda calculus.) A similar graphical language is Chemlambda by Buliga, which uses graph rewrite rules with very similar node types. Programming by drawing things in 2D on a fixed grid is an interesting idea I've wanted to experiment with. (I'd imagined a more Factorio-like Puredata or Max/MSP. It's something that came to mind from having read about [3].) [1] https://ncatlab.org/nlab/show/reflexive+object
[2] https://github.com/Kindelia/HVM/blob/master/HOW.md
[3] https://100r.co/site/orca.html |
|
|
That's a useful pointer. It's interesting that the nLab folks seem to specifically point out higher-order abstract syntax as the underlying intuition behind these 'lam' and 'app' morphisms. So if actual string diagrams exist for these, the same sort of graphical representation may well be applicable beyond the untyped lambda calculus itself, to any syntax that has some equivalent to "variables" that can be used for substitution as in beta-reduction. (Note that the graphical representation of a typed lambda calculus is fairly obvious and intuitive, but only because functions then get different types based on their arity, etc. and this is directly reflected in the visual syntax. Once you go untyped, it doesn't seem that this can be true.)