Hacker News new | ask | show | jobs
by zozbot234 1537 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[ https://ncatlab.org/nlab/show/reflexive+object ]

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.)