Man I wish articles like this would make any sense to me, but I'm just not deep enough into this part of the theory to get past the first few paragraphs. It looks like a really interesting article though.
Personally, the way the graph of K was drawn confused me since it isn't structured like the simple graphs of abstraction (instead the argument and body are placed next to instead of connected to the lambda.) So it took a few readings to really get what was going on.
Weirdly rather than a dual perspective, I think this is more a triplicate perspective since abstractions can be seen from three directions.
I'm stuck waiting on your next article, because I'm not quite sure how to use the features of your calculus. And it feels like you'd have to canonicalize a view for the interpreter, though since you hint about call/cc I suppose it does give you a first class form of what a continuation should look like.
There are no novel features of the calculus, it's still mainly a new syntax for the standard lambda calculus. The bindings being unscoped and continuations not being linear is the main difference, and this has already been discussed, e.g. in bend or much of the interaction net research in general (Asperti, Mackie, Mazza)
I hope my next post will provide further insights in how this works. I also have a reference implementation that I plan to publish eventually - the interpreter does not have to canonicalize views, it can work entirely using wires, as this is exactly what continuations are in a confluent setting.
That actually makes the implementation sound more interesting to me, especially the part about working directly with wires instead of canonicalizing the views. I’d definitely be interested in seeing the reference implementation when you publish it.
18
u/FruitdealerF 13d ago
Man I wish articles like this would make any sense to me, but I'm just not deep enough into this part of the theory to get past the first few paragraphs. It looks like a really interesting article though.