Господа, можете подкинуть какую-нибудь доступную статью о компиляции в interaction nets? Меня прежде всего интересует ответ на вопрос: а зачем в них компилировать? Всё, что нахожу сам, просто описывает технику, но она, вроде, и так понятна.

#fpcompiling

За ради optimal reduction?

А как она следует?

Её же на interaction nets делают -- значит, нужно сначала скомпилировать в такую сеть. 🤷‍♀

А почему в Haskell и Clean используют редукцию графов, а не вот эти nets?

Не знаю, может, слишком старые? У меня сложилось впечатление, что сети взаимодействия и оптимальную редукцию начали исследовать совсем недавно и всё ещё продолжают.

На эту тему же было весёлое: https://medium.com/@maiavictor/some-functions-may-have-negative-complexity-im-worried-for-my-crypto-c53f6e7343d3

оно ещё вроде позволяет параллелить мощно

@Comonoid этой темой занимается интенсивно последнее время

Да. Вот это и сборка мусора особо интересуют. Потому что, кажется, можно технику перенести не только на лямбда-исчисление но и на futures, и потом на распределённые вычисления.

А если, например, взять старую-добрую Линду и доработать ее (на самом деле, скорее, ограничить) по части линейных кортежей — это будет не оно? ;)

интеракционные сети это и есть формализм, выросший из ограничений на деревья вывода линейной логики

Заявлены были параллелизм и отсутствие сборки мусора. И я вношу интригу — формализм против другого формализма :) Линда, конечно, штука скучная и немодная, о ней пишут в любом учебнике по моделям параллельных вычислений. Но подходит же? :)

линда это ж вроде разновидность процесс алгебры

Линда — это такой маленький eDSL для распределенных вычислений.

И операция in(t) в Линде очень в духе работы с линейными объектами. То самое destructive read :)

Вообще, я бы больше доверял работам, где формализм применяется для решения прикладных компиляторных задач. Где, по крайней мере, видно, как можно сократить разрыв между отвлеченной формализацией и инженерной практикой.

Но случается, кстати говоря, и иная ситуация. Накануне я критиковал LLHD как раз за  недостаточную «идейность». В это смысле интересно наблюдать, что читателям новостей и блогов ближе свободолюбивый активизм LLHD, а не важные, новые подходы того же AnyHDL.

Та же история с недавним языком высокоуровневого описания аппаратуры Dahlia, где используется, кстати говоря, линейная логика. Но упоминания о Dahlia вы на хабре не встретите (в отличие от LLHD). А вот в нашем чате — запросто:

https://arxiv.org/pdf/2004.04852.pdf

Я не видел децентрализованных реализаций Линды. Не думаю, что это вообще возможно.

А что мешает?

Имена надо как-то синхронизировать постоянно. Не понятно, возможно ли это делать без сбора всей иныормации на одном узле. Там же не доказывается, что от порядка операций ничего не зависит.